Formalization of the OpenAI Proof Withdrawal
github.com
github.com
1) You are the author of ityonemo/openai-wiles?
2) It uses a program "2b4m" that was also made by you?
3) The program 2b4m tries to prove the "Weil-classes" following the OpenAI manuscript and fails because the manuscript is wrong?
4) If you use "magic" to add the mistake in the sign then the program 2b4m can complete a fake proof that use the magic?
5) The main idea is that 2b4m can write human readable proof that can be verified by the computer.
[Unlike Lean that is difficult to read by humans and English that is difficult to read by the computer. I hope I don't annoy too much any Lean of English fan.]
---
More questions:
6) Can 2b4m compile/transpile a correct proof to Lean or it has it's own engine?
7) This manuscript cites another paper that is not formalized, so the result of the other paper is added using magic too? (In spite the other paper is probably correct and it's just a matter of time until someone can replace the magic with a computer readable proof.)
8) Can 2b4m import Lean code/libraries in particular Mathlib?
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!
IIUC a typical 2b4m proof is longer than the idiomatic Lean proof.
8) FOL -> First Order Logic, I guess.
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.