It may help to look at this example concretely: The natural-language statement of the problem is (from https://www.erdosproblems.com/728 https://www.erdosprobl

It 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.)