That's not HTML though, you have to learn a whole new dsl that must conform to rust parser rules. So, not the same thing at all.

If I understand lean you have a bag of facts and it goes and searches for any fact that matches the right shape. 2b4m is explicit, you provide the fact dependency. Lean is more "designed for humans to write" in its ethos.

2) yes

3) Here's what 2b4m can show:

- simulate the convention error as a mistranscribed previous result (convention error and mistranscription are, AFAIK, equivalent constructions)

- assuming the mistranscribed previous result, the entire proof is logically consistent

- if you "correctly transcribe" the previous result, the proof fails in the expected position

3) no (like lean, I do not have the tower of math results that Weil classes needs)

4) yes. the "fake proof" is the proof that OpenAI submitted.

5) that's the general idea, Lean proofs are human readable, but they aren't naively readable. I can't hand a random math major that has no lean training a proof and expect them to validate it. The tradeoff is tediousness. 2b4m proofs are crazy tedious (hence the name).

6) it has its own engine, so yes, the kernel may have errors. Transciption to lean is a planned feature.

7) Yep, I'm not an expert in Weil-classes, so it's possible that the AI mistranscribed the math proofs in the literature. It's also possible that the math proofs in the literature have been incorrectly validated by the community.

8) no. Strictly cannot. IIUC Lean proofs can rely on higher order logic, 2b4m explicitly is FOL only, though there are some "nice constructions" that look like higher order logic but are actually just symbolic transformations that are designed to recapitulate how mathematicians think when they use cross-domain facts.

Postscript I just realized (thank you) that I misnamed the repo "openai-wiles" instead of "openai-weil" humans make mistakes too!

Interestingly, if you shim the well-known theorems, it does not uncover the error in the proofs (tldr there are competing conventions for tracking an invariant which make theorems incompatible) which are not obvious unless you work in the field I guess? A theorem checker cannot check the compatibility of conventions unless you go ALL the way to the mathematical roots.

If you're interested in a formalization of the retracted proof by openai (apologies for the LLM-speak in the documentation, but that is the point, can LLMs do XYZ):

https://github.com/ityonemo/openai-wiles

Comments URL: https://news.ycombinator.com/item?id=50023433

Points: 3

# Comments: 5

The branching does not cost as much as you think, I'm pretty sure the compiler marks the erroring path as cold, which the cpu can use to elide most of the branch cost through specex

on a surface level a human solving an (unsolved) math problem can look like this, and of course the tree of all possible symbols you can send to a proving assistant is much wider than what the human samples, and the same goes true for an LLM in a proving loop. It isn't "truly random", it can't possibly be (and solve the problem). Both humans and LLMs solving unsolved math problems are aggressively pruning mathematical syntax and logical strategy trees.