None of the papers withdrawn were formalized in Lean, only about half the papers in the repo are formalized. I don't think we yet have an example of what you're suggesting actually happening.

▲

ijustlovemath 4 hours ago | parent | next [-]

I also don't think there's been nearly enough time for peer review of what was actually formalized vs what was intended. How many humans out there actually have a deep enough understanding of the background to be able to check the work? I understand that Lean checks the mechanical steps, but if it's building a ladder to some other result entirely, nobody (certainly nobody on HN) will know for some time.

I'm probably wrong, but what's the point of throwing away all skepticism?

▲

jrflo 3 hours ago | parent | next [-]

You only need the problem statement to be correct in Lean, no matter what route it goes down is correct as long as the original formalization of the problem is correct, which is substantially easier to check. Not sure how many people have checked that so far, but I'm guessing the math community would be quick to point out if something basic like that was missed for something like a new bound on RH.

Nothing wrong with being skeptical, but I see no reason to be skeptical as of yet.

▲

JacobAsmuth 5 minutes ago | parent | next [-]

There's nothing to check there, they used the standard mathlib implementation of RH. THey didn't write their own for the 7/8ths proof.

▲

techblueberry 3 hours ago | parent | prev [-]

Were days out, the default should probably be skepticism for about a decade.

	▲	juanani an hour ago \| parent [-]
		[dead]

▲

auggierose 3 hours ago | parent | prev [-]

Again, you don't need to check the proof, Lean does that. You need to check the statement, which is a much easier task. So yes, you are wrong. Skepticism is good, but it is usually just ignorance.

▲

mirashii 3 hours ago | parent | prev [-]

Here's a recent example of an AI exploiting a soundness hole in Lean in a paper purporting to have solved the Collatz Conjecture.

https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...

There's also a fairly well known incident where the Lean formalization of the Riemann Hypothesis in Mathlib was incorrect.

	▲	Chinjut 3 hours ago \| parent [-]
		This paper "purporting to have solved the Collatz conjecture" was essentially a deliberate joke. It was not a serious attempt to prove the Collatz conjecture, it just used that framing to deliberately point out a Lean soundness bug. The soundness bug is real, but the idea that this was something you might accidentally run into while trying to prove the Collatz conjecture is made up.