thom

Alright Oppenheimer, calm down.

Dune: Prophecy is set after the Butlerian Jihad (which is why the presence of an AI is controversial).

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?

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!

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?

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.

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.

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.

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.

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.

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.

It’s a go!

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