Mathematicians have come up with formal languages that can, in principle, be used to write proofs in a way that they can be checked by a simple algorithm. However, they’re utterly impractical.
I understood that a part of the univalent foundations project is to develop a base formalism for mathematics that’s amenable to similar layered abstraction with formal proofs as you can do with programs in modern software engineering. The basic formal language for proofs is like raw lambda calculus, you can see it works in theory but it’d be crazy to write actual stuff in it.
So is it possible that in the future we might be able to have something that’s to the present raw proof languages as Haskell is to basic lambda calculus, and that it might actually be feasible to write proofs on top of established theorem libraries with the highest level of proof code concise enough for comfortable human manipulation?
I also understand that Coq does some limited proof search based on the outline given by the human operator, which is another interesting usability groove on top of the raw language. Of course both using a complex, software-engineering like theorem library and giving proof-hints to a Coq style program are pretty obvious expert skills which you’ll expect to have after being quite familiar with knowing how mathematical proofs work in general.
I understood that a part of the univalent foundations project is to develop a base formalism for mathematics that’s amenable to similar layered abstraction with formal proofs as you can do with programs in modern software engineering. The basic formal language for proofs is like raw lambda calculus, you can see it works in theory but it’d be crazy to write actual stuff in it.
So is it possible that in the future we might be able to have something that’s to the present raw proof languages as Haskell is to basic lambda calculus, and that it might actually be feasible to write proofs on top of established theorem libraries with the highest level of proof code concise enough for comfortable human manipulation?
I also understand that Coq does some limited proof search based on the outline given by the human operator, which is another interesting usability groove on top of the raw language. Of course both using a complex, software-engineering like theorem library and giving proof-hints to a Coq style program are pretty obvious expert skills which you’ll expect to have after being quite familiar with knowing how mathematical proofs work in general.