bluesky — Antonio E. Porreca 🐳 — 20 Sep 2026
Even if proof checking is a part of maths (it’s not, in any mainstream way) or will be (which I don’t particularly belie…
#proof-assistants #formalization #mathematical-practice
Even if proof checking is a part of maths (it’s not, in any mainstream way) or will be (which I don’t particularly believe), it does not give the output. If we are interpreting “output” in the most restrictive way (and we shouldn’t), the output of maths is a paper or a book or a talk, not Lean code.