Item — HN Reader

That is basically the pitch for Metamath Zero[0].

I'm philosophically aligned with you. Basically, I think this is because of where resources are invested - there's a tremendous amount of work on programming languages to make them ergonomic and enable composition of pieces. Much of that work is at its essence processing friendly syntax into some form of typed lambda calculus. Since dependently typed lambda calculus is a very handy way to encode proofs, it's easier to just adapt that all that mechanism than to develop infrastructure just for proofs.

Interop is hard, because all the axiom systems tend to be subtly different in ways that are hard for normal people to appreciate, though there is some work on it, including MM0.

[0]: https://github.com/digama0/mm0

1 comments

> Interop is hard, because all the axiom systems tend to be subtly different in ways that are hard for normal people to appreciate, though there is some work on it, including MM0.

Would it be tenable to build a parameterized axiom-system-evaluation-engine for which the semantics of a specific proof-assistant would consist of a configuration for this general engine, rather than patches to its code?

If so, would it then be possible for interop to happen "between" proofs in slightly-different axiom systems, the way that regular hand-written "translational" proofs work in mathematics — i.e. "take this property we've proved, translate it into domain model X, derive a property Y, then translate property Y back out of domain model X and into domain-model Y, where we actually want to use it?" — but all under-the-covers, as the (proven) equivalent of FFI, autogenerated as glue proof-code by analyzing the differences between two "configurations" to the engine?