This is (unfortunately) not actually the case—just a few weeks ago, someone "proved" the Collatz conjecture via a Lean proof 1) whose theorem statement was correct, 2) typechecked, and 3) was even verified by external tools with their own implementations of the kernel.[0]

The problem was (AFAIK) that the Lean kernel has a lot of fancy features that aren't yet perfectly understood from a type-theoretic perspective (I don't think Lean is unique in this regard; pretty sure Rocq and Agda are in a similar situation). And so when the kernel implements some feature whose soundness isn't guaranteed, the independent verification tools (or at least some of them) follow suit, and now any issues in the former affect the latter as well.

[0] See e.g. https://x.com/gro_tsen/status/2082483878480977959 for more detail

[0] https://en.wikipedia.org/wiki/Byzantine_Empire#Nomenclature

> Don't post generated text or AI-edited text. HN is for conversation between humans.

(I'm not a mod or anything; I just noticed that most of your comments have been flagged/killed, and I suspect this might be why.)

[0] https://news.ycombinator.com/newsguidelines.html

Of course it'd be super helpful to have, say, a teacher who could tailor explanations to anyone's precise background (e.g. where possible, using examples that come from the student's field of study when explaining some abstract concept). Or, if some definition comes with some precondition that has no obvious purpose, perhaps an omniscient teacher could explain why it's there with concrete counterexamples.[0] But even granting all this, I think that mathematical intuition is necessarily based on a lot of hard work actually exploring definitions on one's own, with pencil-and-paper and a lot of thought. That is to say, even though the process could probably be sped up a lot with a nigh-omniscient teacher[1], I doubt that a student wouldn't still need years of training to even have a clue what's going on.

(I'm saying all this, by the way, as someone who is terrible at all this and has very little mathematical maturity[2]—I'm speaking from my own frustrating experience....)

[0] c.f. Lakatos' excellent book Proofs and Refutations

[1] without the "curse of knowledge," or else we're back to square one of "answers that are correct but useless"

[2] e.g. the "post-rigorous stage" described in https://terrytao.wordpress.com/career-advice/theres-more-to-...

Indeed, that is (allegedly) the case with organ donation: https://www.nytimes.com/2025/07/20/us/organ-transplants-dono...

Here's hoping the idea is that the slices will be really small, or something, because frankly the whole thing is utterly horrifying enough as-is.

Frankly, this comment feels almost entirely foreign to my experience—I suppose things could've changed over the years (although my impression is that things have gotten much worse recently, not better), or it could be major-specific, or I just got lucky with the specific people I happened to hang out with?

> Be kind. Don't be snarky. Converse curiously; don't cross-examine. Edit out swipes.

While we're at it, I'm under the impression that the recent LLMs have also co-opted "genuinely", which I'll never forgive them for—first they stole my em-dashes, and now they're stealing my adverbs too?!