Post #2920387
2026-05-10 20:06 UTC
@tao@mathstodon.xyz there is an ethical/philosophical component to the third component in particular. The food analogy it too crude here.
For a proof is only really digestible if there is a maths community consensus on it.
There are maths examples of similar situations in the pre-LLMs era: 4-colouring problem, CFSC --classification of the finite simple groups, etc.
These demonstrate indigestible proofs, with constant (although seemingly running out of steam) more or less (less in the CFSC case) successful attempts to improve their digestibility.
These also demonstrate the social side of indigestibility - CFSC declared "complete" by the main driving forces of the program, in part for reasons of finances, well ahead of real completeness resulted in the crumbling of the program.
A similar, but much larger in scale, affecting all the branches of the maths, crumbling would occur if top mathematicians started to declare maths "solved" - in exchange for being showered by grants from LLM/AI dealers. And this seems to be happening already.
Replies (1)
-
@screwlisp@gamerplus.org 2026-05-12 05:14
@dimpase@mathstodon.xyz @tao@mathstodon.xyz by the way, someone asked me in this context why a formal proof written for a formal proof checker would need to be reviewed. In this case I guess the answer is that a program of a valid proof needs to be checked that it is a formalisation of the informal description. So validatable formal text of a proof technically existing somewhere does not mean anything if there is not a skilled human in the loop. The utf8 sequence of the proof will exist somewhere inside pi, right.