|
|
|
|
|
|
by ratmice
477 days ago
|
|
|
I am talking not about the ability to typeset your proofs, but the source code itself for the proofs. At the very least all the Isabelle and Coq proofs I've looked at have look much more like source code than the proofs they formalize. |
|
|