4 ms·
I guess the hope is that eventually there will be a language which is roughly as easy to read/write as normal proofs in English but can be machine checked. Lea
by sebzim4500 3y ago
I guess the hope is that eventually there will be a language which is roughly as easy to read/write as normal proofs in English but can be machine checked.
Lean comes closer than Coq, but is still far from this ideal. It may be that AI will need to be involved (as in, there could be a tactic that generates proof terms using an transformer or something).
- hgsgm 3y agoLike Cobol? Coqobol?
- zozbot234 3y ago> I guess the hope is that eventually there will be a language which is roughly as easy to read/write as normal proofs in English but can be machine checked. That's what "declarative proofs" are for (as seen in Mizar, Isar, and formerly in the Coq plugin C-zar). Most proofs in interactive proof assistants are written as "proof scripts", which cannot be understood without playing them back in the proof assistant (in fact, specifically the version of the proof assistant that the "script" was originally written for) and checking how each step in the "script" relates to the current proof state. Declarative proofs are more self-contained, in that the assumptions and conclusions involved in each proof step can be ascertained by just reading them in the code. They can also be naturally simplified into structural "proof sketches", where missing steps in the proof could potentially be filled by a proof-searching "AI".
- creata 3y ago> in fact, specifically the version of the proof assistant that the "script" was originally written for Are Isar updates guaranteed not to break proofs?
- edflsafoiewq 3y agoI think you'll get machines that can check human proofs first.
- sebzim4500 3y agoI think the only way to do this that anyone will find convincing is to have an LLM turn the human proof into a machine checkable one, so all the research into Lean etc. will still be useful.