Do you have a dumb question that you're kind of embarrassed to ask in the main thread? Is there something you're just not sure about?
This is your opportunity to ask questions. No question too simple or too silly.
Culture war topics are accepted, and proposals for a better intro post are appreciated.
Jump in the discussion.
No email address required.
Notes -
Theorem provers do all of the evaluation work ... for those specific results which have been painstakingly translated into the theorem prover's language, which to a first order approximation is zero percent of the new and interesting results.
Training a transformer AI on MetaMath (or on Coq results, whatever large database has both complete proofs and adequately verbose comments), combined with the verifier itself, might be enough at this point to create a "math-paper to formal-proof" translator. Skimming through comments I see a lot of links back to the papers which originally published each theorem, which certainly ought to qualify as "adequately verbose" even if the database comments themselves are fairly terse.
Doing creative work would of course be more interesting ... if we could only define what's "interesting". 378+135=513 is a theorem among infinite others, but nobody cares about it. We tend to like math if it eventually has endpoints with real-world applications, and it's a bit hard to put that into an evaluable loss function. We also tend to like theorems if they're more general, and if they're short to state but long to prove, and if they're on the shortest path to proving other theorems, and maybe there's something to those criteria that could be quantified well enough to point a Neural Net Monte Carlo Tree Search in the right direction?
More options
Context Copy link