All Questions
Tagged with formal-languages proof-assistants
2 questions
3
votes
0
answers
406
views
Conversion of proofs between HoTT and ZFC
HoTT provides a foundation of math that remains mysterious for
many mathematicians including me. Hence this question.
There are several implementations of math based on ZFC, an
example being MetaMath. ...
- 5,230
6
votes
3
answers
1k
views
Proof formalization
I read some time ago some papers about proof formalization. Typically, I began whith this one, from Lamport.
Are there more recent works in this field ?