6 ms·
How do you verify that the AI translation to Lean is a correct formalization of the problem? In other fields, generative AI is very good at making up plausible
by aidenn0 10mo ago
How do you verify that the AI translation to Lean is a correct formalization of the problem? In other fields, generative AI is very good at making up plausible sounding lies, so I'm wondering how likely that is for this usage.
- roenxi 10mo agoYou're looking for the practical answer, but philosophically it isn't possible to translate an informal statement into a formal one 'correctly'. It is informal, ie, vaguely specified. The only certain questions are if the formal axioms and results are interesting which is independent of the informal formalisation and that can only be established by inspecting the the proof independently of the informal spec.
- wizzwizz4 10mo agoPhilosophically, this is not true in general, but that's for trivial reasons: "how many integers greater than 7 are blue?" doesn't correspond to a formal question. It is absolutely true in many specific cases. Most problems posed by a mathematician will correspond to exactly one formal proposition, within the context of a given formal system. This problem is unusual, in that it was originally misspecified.
- red75prime 10mo agoI suppose there's no formally defined procedure that accepts a natural language statement and outputs either its formalization or "misspecified". And "absolutely true" means "the vast majority of mathematicians agree that there's only one formal proposition that corresponds to this statement".
- varjag 10mo agoI think you suppose wrong. A statement like "the area of the square whose side is the hypotenuse is equal to the sum of the areas of the squares on the other two sides" doesn't seam out of reach of an algorithmic procedure like a classical NLP.
- red75prime 10mo agoSure, we can write a procedure that recognizes some formal grammar, which intersects with the natural language. Defining the formal grammar that fully captures the current natural language understanding of the mathematical community is a bit harder.
- wizzwizz4 10mo agoThis problem was even worse: it's matched by the formal grammar, but the naïve formalisation has a trivial answer, so it is clearly not what was intended.
- NetMageSCW 10mo agoThat clearly may be doing some heavy lifting. It is assumed that trivial answer wasn’t what was intended for the problem, but unless someone asked Erdos, I don’t think we know.
- wizzwizz4 10mo agoConsidering that he did some work towards the problem, tackling non-trivial cases, I think we do know. There's no way he wouldn't have perceived trivial solutions at some point.
- sibrahim 10mo agoThat's what's covered by the "assuming you have formalized the statement correctly" parenthetical. Given a formal statement of what you want, Lean can validate that the steps in a (tedious) machine-readable purported proof are valid and imply the result from accepted axioms. This is not AI, but a tiny, well reviewed kernel that only accepts correct formal logic arguments. So, if you have a formal statement that you've verified to represent what you are interested in by some other means, Lean can tell you whether the proof created by genAI is correct. Basically, there is a nigh infallible checker that won't accept incorrect hallucinations.
- mjevans 10mo agoI think the question is, how can humans have verification that the problem statement was correctly encoded into that Lean specification?
- mrtesthah 10mo agoThey probably need to be able to read and understand the lean language.
- aidenn0 10mo agoI can read and understand e.g. Python, but I have seen subtle bugs that were hard to spot in code generated by AI. At least the last time I tried coding agents (mid 2025), it was often easier to write the code myself then play "spot the bug" with whatever was generated. I don't know anything about Lean, so I was wondering if there were similar pitfalls here.
- mkehrt 10mo agoIn this case the human written statement of the theorem is small. Can there be bugs? Absolutely! But it's essentially a few lines of code worth of thinking. The lean proof checker then checks to make sure the proof actually proves the statement. In this case an AI is generating the proof, but if it "compiles" it's correct. The only thing humans need to check is the statement to be proven. (I don't know anything about this project but I've played around with lean and used other proof checkers more sesrisously).
- jlouis 10mo agoThe statement is something you provide. It's the search you can have the LLM do. If this works for math it will immediately make code way higher quality via the same tools.
- maxwells-daemon 10mo agoFor this reason, when we announce results on e.g. the IMO, we formalize the statements by hand and inspect the proofs carefully to ensure they capture the full spirit of the problem. However, there are some good heuristics. If you expect a problem to be hard and the proof is very short, you've probably missed something!
- bytesandbits 10mo agono you don't https://www.reddit.com/r/singularity/comments/1pv3nl3/comment/nvtlgqb/?utm_source=share&utm_medium=web3x&utm_name=web3xcss&utm_term=1&utm_content=share_button https://www.reddit.com/r/singularity/comments/1pv3nl3/commen...
- minitech 10mo agoThat doesn’t look like a counterexample to “we formalize the statements by hand and inspect the proofs carefully to ensure they capture the full spirit of the problem”.
- tomjen3 10mo agoAren't the best proofs very short?
- j_maffe 10mo ago"Best" is subjective. Proofs can get very long especially for the harder ones mathematicians are tackling these days.
- rtpg 10mo agoI feel like even outside of AI translation, formalization not capturing the spirit of what the informal description was provided is always a risk. This is also a big risk when trying to prove code correctness: "prove this algo works" means you gotta define "works" along certain axes, and if you're very unlucky you might have a proof that exploits the uncertainty around a certain axis.
- maccam912 10mo agoTo answer the question a different way, I think you are asking how we know the proof actually matches the description the human provided? And I'd say we can't know for sure, but the idea is that you can pretty concisely write and check yourself that the problem is accurate, i.e. "There are an infinite number of primes" or whatever, and then even if an LLM goes off and makes up a lean proof wildly different from your description, if lean says the proof is valid then you have proven the original statement. I guess in theory the actual proof could be way different than what you thought it would be, but ultimately all the logic will still check out.
- svat 10mo agoIt may help to look at this example concretely: The natural-language statement of the problem is (from https://www.erdosproblems.com/728 https://www.erdosproblems.com/728): > Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn? The Lean-language statement of the problem (which can be done either by hand or by AI) is (from https://github.com/plby/lean-proofs/blob/f44d8c0e433ab2855411c7c3ea321eece66e3911/src/v4.24.0/ErdosProblems/Erdos728b.lean#L1366-L1374 https://github.com/plby/lean-proofs/blob/f44d8c0e433ab285541...): ∀ᶠ ε : ℝ in [>] 0, ∀ C > (0 : ℝ), ∀ C' > C, ∃ a b n : ℕ, 0 < n ∧ ε * n < a ∧ ε * n < b ∧ a ! * b ! ∣ n ! * (a + b - n)! ∧ a + b > n + C * log n ∧ a + b < n + C' * log n Yes on the one hand, one needs to know enough about Lean to be sure that this formulation matches what we intend, and isn't stating something trivial. But on the other hand, this is not as hard as finding an error on some obscure line of a long proof. (There's also an older formulation at https://github.com/google-deepmind/formal-conjectures/blob/ff51e6a91df774fd96674189bd7696f26a043a74/FormalConjectures/ErdosProblems/728.lean https://github.com/google-deepmind/formal-conjectures/blob/f... but the new one is more in the spirit of what was intended: see the discussion starting at https://www.erdosproblems.com/forum/thread/728#post-2196 https://www.erdosproblems.com/forum/thread/728#post-2196 which gives a clear picture, as of course does Tao's thread in the OP that summarizes this discussion.)
- kovek 10mo agoI'm wondering how do people come up with these mathematical challenges?
- mikhailfranco 9mo agoLive out of a suitcase, travel the world, hang out with a wide selection of excellent mathematicians, write joint papers with many of them, when you get bored or stuck, pack the suitcase and keep moving - for your whole life.
- JacobAsmuth 9mo agoYou read it yourself :) If you and the AI agree on the translation of the problem, and lean agrees with the solution, then you're done.