When Computers Write Proofs, What’s the Point of Mathematicians?

Is math just symbol pushing? Quanta and a Lean prover demo on the social side of mathematical proof.

Is math just symbol pushing?

When Computers Write Proofs, What’s the Point of Mathematicians? [1]

Article: [2]

Lean theorem prover: [3]

Originally posted on LinkedIn.

---

References

[1] Quanta Magazine. “When Computers Write Proofs, What’s the Point of Mathematicians?” (video). https://youtu.be/3l1RMiGeTfU

[2] “Why Mathematical Proof Is a Social Compact.” Quanta Magazine, August 31, 2023. https://www.quantamagazine.org/why-mathematical-proof-is-a-social-compact-20230831/

[3] Lean theorem prover. https://leanprover.github.io