“A class of statement between conjecture and theorem” by Jason Fantl

Parts of the math community, such as Henry Cohn and Grant Sanderson, are arguing that proofs have been a proxy for understanding, and now that proxy is broken. This is a response to LMs generating incomprehensible proofs, often formalized in Lean. While the proofs are verified, they lack the pedagogical value which has historically come along with new proofs. In the past we could typically assume at least one human in the world understood the novel insight required to produce a proof, but that assumption no longer holds.

I suspect we will need a new class of statement which contains statements which are proved but not understood, something the mathematical community can formally recognize as a contribution to the field. The understanding gives us the tools to do math, and the proof verifies that our understanding is correct, so we should ensure we have the language to communicate the state of both.

For now I will call this class of statement a compertum (Latin, neuter of compertus, ascertained; from comperire, to find out for certain). A conjecture is from the Latin conicere, to throw together: an inference assembled from the evidence. A theorem is from the Greek theōrēma [...]

The original text contained 1 footnote which was omitted from this narration.

---

First published:
September 21st, 2026

Source:
https://www.lesswrong.com/posts/ZnNvci7jk9qEGr3z3/a-class-of-statement-between-conjecture-and-theorem

---

Narrated by TYPE III AUDIO.

---