This is great to see. I was at UChicago and remember Eugenia Cheng giving a talk about this. It profoundly affected my perspective on mathematics and the goal of mathematical proof… that mathematics is ultimately about more than just lists of true theorems.

Thurston’s On proof and progress in mathematics feels related. Or the “literate programming” conceit that programs are written first for human insight. I often wonder how all this connects to “proofgramming” and the interest in the formal verification of mathematics.

See also “Social processes and proofs of theorems and programs” for an unduly pessimistic but insightful take on the implications of “social proof” in mathematics for formal verification of software.

Oh hey, Eugenia Cheng taught me in my first year of my undergrad at Sheffield. I remember her dropping hints about intuitionism while teaching us number theory.

This is great to see. I was at UChicago and remember Eugenia Cheng giving a talk about this. It

profoundlyaffected my perspective on mathematics and the goal of mathematical proof… that mathematics is ultimately about more than just lists of true theorems.Thurston’s On proof and progress in mathematics feels related. Or the “literate programming” conceit that programs are written first for human insight. I often wonder how all this connects to “proofgramming” and the interest in the formal verification of mathematics.

See also “Social processes and proofs of theorems and programs” for an unduly pessimistic but insightful take on the implications of “social proof” in mathematics for formal verification of software.

Oh hey, Eugenia Cheng taught me in my first year of my undergrad at Sheffield. I remember her dropping hints about intuitionism while teaching us number theory.