Hacker News: thom

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Sat, 03 Oct 2026 15:05:28 +0000

So the types of errors in that paper could never lead a mathematician to make a claim about a Lean proof that was later found to be incorrect?

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Sat, 03 Oct 2026 13:14:35 +0000

Right but... the difference between "a robot may not injure a human being" and "a robot must injure a human being" is quite important in the real world, even if the "mathematical content is correct". And if my silly example is too contrived, it still seems like this sort of thing happens all the time:

https://proceedings.mlr.press/v306/ammanamanchi26a.html

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Sat, 03 Oct 2026 13:05:01 +0000

How would you characterise the 4833 issues surfaced by this work?

https://proceedings.mlr.press/v306/ammanamanchi26a.html

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Sat, 03 Oct 2026 12:53:48 +0000

Lemme give an example of the kind of thing I'm picturing and you can tell me where it goes wrong. Lean Web tells me the following is fine:

  import Mathlib

  abbrev Scalar := ℂ
  abbrev Real := Scalar

  theorem negative_one_has_a_real_square_root :
      ∃ x : Real, x * x = -1 := by
    exact ⟨Complex.I, Complex.I_mul_I⟩

But we know it's a lie. I hide those abbrevs in 100k lines of stuff that you haven't yet checked manually. I don't understand what could be stopping shenanigans like these, though I appreciate you trying to show me!

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Sat, 03 Oct 2026 10:22:20 +0000

Okay this is more revealing, thank you. You’re saying that A and C are very small, humanly verifiable pieces of encoded logic. Can you give me an example of how Bs come into being and why they can never be wrong?

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Sat, 03 Oct 2026 10:11:10 +0000

Yes but why do we write the last bit as an aside as if that’s not a massive yawning black hole for errors to hide in? All the other stuff is irrelevant, just like when Haskell and Rust people claim that if their code compiles it is correct.

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Sat, 03 Oct 2026 10:09:46 +0000

Surely “the proof is the one you think it is” is the whole ballgame? Why is it impossible for a condition to be subtly reversed somewhere in the code, rendering the entire proof useless In the real world? I’m begging for an explanation of why this is impossible because I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Sat, 03 Oct 2026 06:35:32 +0000

How many new lines of Lean do these recent Millennium Prize proofs introduce on top of known good axioms? I suppose I’m asking what the actual workflow is to inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is, because I know of no other substantial source code produced by LLMs that has literally zero bugs, however strong the type system of the language it’s writing in.

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Sat, 03 Oct 2026 06:29:04 +0000

Hidden like any subtle bug that one might gloss over when inspecting the source code. The statement you’re trying to prove could be thousands of lines long and that semantic mismatch could occur anywhere. We seem to be very blasé about this.

New comment by thom in "Anatomy of a Lean proof for software engineers"

thom — Fri, 02 Oct 2026 22:57:29 +0000

So this is all great, but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan? These seem like uniquely fragile software artifacts, despite the excellent and robust promises made by the runtime.

New comment by thom in "Why media fans want to escape algorithms with CDs, DVDs and vinyl"

thom — Fri, 02 Oct 2026 11:57:33 +0000

My experience also. I discover new music at a higher rate than even my teens when I listened to the radio every night, and went to gigs and bought CDs weekly. I still have some music I have to use my own MP3s for but I feel incredibly well served by streaming.

New comment by thom in "SpaceX's Starship launching to orbit for first time ever today"

thom — Mon, 28 Sep 2026 13:12:53 +0000

It’s a go!

New comment by thom in "Postgres SELECT DISTINCT Does Not Scale"

thom — Sat, 26 Sep 2026 10:11:55 +0000

Yeah, it's almost always more intention-revealing to use CTEs and WHERE EXISTS.

New comment by thom in "Why I'm still bearish on LLMs after Navier-Stokes"

thom — Wed, 23 Sep 2026 13:50:00 +0000

Yes, we can come up with all sorts of weird situations where you can get it to be confused. But what I'm saying is it's _trivial_ to give it a simple prompt that prevents it from ever making any errors, and so I don't think it's this big LLM gotcha (of which there are many!)

New comment by thom in "Why I'm still bearish on LLMs after Navier-Stokes"

thom — Thu, 17 Sep 2026 09:27:44 +0000

Humans do make these errors when playing blindfolded. If you even the playing field and give the LLM the position at each turn, it does not make mistakes.

New comment by thom in "Why I'm still bearish on LLMs after Navier-Stokes"

thom — Wed, 16 Sep 2026 15:39:35 +0000

I maintain that the amount of effort to teach a human to do this vastly outweighs the amount of effort to teach an LLM to do this unless you're deliberately trying to make them fail. I honestly have no bigger point than that, I just think this isn't a very good thing by which to evaluate LLM capabilities. If there's no argument you'll accept, I am happy to move on.

New comment by thom in "Why I'm still bearish on LLMs after Navier-Stokes"

thom — Wed, 16 Sep 2026 13:10:11 +0000

A human wouldn't do that, they'd look at the board. I'm not disagreeing that to demonstrate clear superhuman ability the LLM should be able to do this, but it plays better than most humans blindfolded, and with fair prompts seems very good otherwise.

New comment by thom in "Saving Jet Fuel"

thom — Wed, 16 Sep 2026 11:12:58 +0000

This is sad to hear! Early in my career I worked for a company making airport collaborative decision making (A-CDM) software. One of the most impactful projects to which I contributed was a model that calculated the exact right moment for a pilot to turn their engine on given likely pushback times etc. That saved quite a lot of fuel (and therefore cost and pollution) back in the day. It's a real shame if similar thinking isn't being applied to the problem you describe.

New comment by thom in "Why I'm still bearish on LLMs after Navier-Stokes"

thom — Wed, 16 Sep 2026 10:53:16 +0000

I've not noticed this happening if you give it the FEN each move. The alternative is just blindfold chess and very few humans can do that for long.

New comment by thom in "Why I'm still bearish on LLMs after Navier-Stokes"

thom — Wed, 16 Sep 2026 10:25:46 +0000

How long a prompt do you think would be required to cajole an LLM into making legal moves at the rate of a human? Or do you think no amount of prompting could do that?