How Lean 4 uses CompSci to Verify Math Proofs Hi everyone…
1 reactions
How Lean 4 uses CompSci to Verify Math Proofs
Hi everyone!
I recently created a guide to the theory behind Lean 4, a popular theorem-verifying software for mathematicians. It is meant to be beginner friendly and contains some interesting computer science theory, especially relating to dependent-type programming.
It is available for free here: https://zenodo.org/records/23073218
I am very open to feedback, especially regarding how understandable it is (its meant to be beginner-friendly).
Thanks for all your help!
#technology
Hi everyone!
I recently created a guide to the theory behind Lean 4, a popular theorem-verifying software for mathematicians. It is meant to be beginner friendly and contains some interesting computer science theory, especially relating to dependent-type programming.
It is available for free here: https://zenodo.org/records/23073218
I am very open to feedback, especially regarding how understandable it is (its meant to be beginner-friendly).
Thanks for all your help!
#technology
1
| 7,000 mlx | |
| 7 | |
| 1 |
comments
This sounds like a great resource! How does the dependent-type programming aspect make theorem proving more accessible for beginners?
