All Questions
Tagged with formal-proof proof-assistants
7 questions
5
votes
0
answers
165
views
Formal and informal proofs: Is there any "bilingual corpus"?
There are extensive libraries of formalized mathematics like those of Lean, Coq or Isabelle/HOL. What I am interested in is documents of formalized mathematics that closely follow certain informal ...
- 1,228
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
14
votes
2
answers
1k
views
How does proof assistant organize knowledge?
I am reading a paper
Ittay Weiss, The QED Manifesto after Two Decades — Version 2.0, Journal of Software, 11 no. 8 (2016) pp. 803–815, doi:10.17706/jsw.11.8.803-815
The paper says
Goal 7: ...
- 141
6
votes
0
answers
296
views
formalization of coordinate-free linear algebra in a proof assistant
I am aware of projects that formalize linear algebra in existing proof assistants (i.e. Coq), but it seems like most of them are based on matrices. I was wondering if it's done in a coordinate-free ...
- 161
7
votes
1
answer
759
views
Are there any recent advances in formalizing the undecidability of $\mathit{CH}$?
The website Formalizing 100 Theorems by Freek Wiedijk contains a list of some theorems that were chosen at some point as good candidates for formalization (because of their complexity, their ...
- 1,124
37
votes
1
answer
4k
views
How much mathematics has been formally verified?
That's a vague question so allow me to tighten it up a bit.
I recently noticed that there is a formal machine verified proof of the Central Limit Theorem (CLT) implemented with Isabelle. This ...
- 8,271
59
votes
8
answers
12k
views
How true are theorems proved by Coq?
Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...
- 35.4k