3 ms·
> If not proof trees, what? Just make the proof language similar to the standard mathematics language and possibly process it with a presentation layer that m
by robinzfc 6y ago
> If not proof trees, what?
Just make the proof language similar to the standard mathematics language and possibly process it with a presentation layer that makes it even better. The examples start from Mizar [1] (since 1973), IsarMathLib [2] (disclaimer: my project), Naproche-SAD [3] (bundled with Isabelle recently)
[1] http://mizar.org/ http://mizar.org/
[2] https://isarmathlib.org/ https://isarmathlib.org/
[3] http://ceur-ws.org/Vol-2634/FMM4.pdf http://ceur-ws.org/Vol-2634/FMM4.pdf
- ImprobableTruth 6y agoBut the key difference between Mizar style proofs and Coq/Lean style proofs is just that the former is declarative and the latter is procedural. They're both ultimately just tactics based. Sure, a declarative style is nice when reasoning about equations, but otherwise the proofs simply degenerate into awkwardly written procedural tactics proofs.