Sign up or log in for free. It helps support the project and unlocks personalized paper recommendations and new AI tools. .
Computational tools might tempt us to renounce complete certainty. By forgoing of rigorous proof, we could get (very) probable results for a fraction of the cost. But is it really true that proofs (as we know and love them) can lead us to certainty? Maybe not. Proofs do not wear their correctness on their sleeve, and we are not infallible in checking them. This suggests that we need help to check our results. When our fellow mathematicians will be too tired or too busy to scrutinize our putative proofs, computer proof assistants could help. But feeding a mathematical argument to a computer is hard. Still, we might be willing to undertake the endeavor in view of the extra perks that formalization may bring—chiefly among them, an enhanced mathematical understanding.
Login to see paper summary
| Action | Title | Date | Authors |
|---|
| Action | Title | Date | Authors |
|---|---|---|---|
| A FORMAL PROOF OF THE KEPLER CONJECTURE | 2017-01-01 | Thomas Hales Mark Adams Gertrud Bauer TAT DAT DANG John Harrison Hoang Le Truong Cezary Kaliszyk Victor Magron Sean McLaughlin TAT THANG NGUYEN | |
| On proof and progress in mathematics | 1994-01-01 | William P. Thurston | |
| The Last Universal Mathematician | 1994-06-01 | John Horgan | |
| Reliability of mathematical inference | 2020-01-14 | Jeremy Avigad | |
| Varieties of mathematical understanding | 2021-02-22 | Jeremy Avigad | |
| Who's Afraid of Mathematical Diagrams? | 2021-12-29 | Silvia De Toffoli | |
| Mathematical problems | 2000-06-26 | David Hilbert | |
| Mathematics without Apologies | 2015-07-29 | M. P. Harris | |
| Some thoughts on automation and mathematical research | 2024-02-16 | Akshay Venkatesh |