Once upon a time, John Wentworth and I thought we had a proof of a very useful looking theorem. We did not have that proof. An important intermediate step was shown to be invalid and the whole thing crumbled and disappeared, never to see the light of day again...

Until now! I'd love to say that we came up with an ingenious fix to the old erroneous proof, but unfortunately it turned out to be a really infuriatingly hard nut to crack. Instead I spent the last ~month experimenting with various ways of incorporating frontier LLMs into the proof-making process, specifically with autoformalization and proving in Lean4. (This is, I recently learned, roughly what Resolution is doing.) The result is stated below, and linked at the bottom is a Lean statement+proof of the same.

I will not be providing the proof in prose in this post, as it is not suitable for even impolite human company, but it sure does compile and comes out the other side with a machine-certified proof of what sure looks to be (an even stronger) correctly-expressed statement than the one I was originally aiming for.

Take a look at the first section of [...]

---

Outline:

(01:30) The Statement

(03:50) C

(04:39) Next Steps

The original text contained 5 footnotes which were omitted from this narration.

---

First published:
August 10th, 2026

Source:
https://www.lesswrong.com/posts/TgboJpeN95bs84odk/redux-stochastic-natural-latent-implies-deterministic

---

Narrated by TYPE III AUDIO.

“Redux: (∃ Stochastic Natural Latent) Implies (∃ Deterministic Natural Latent)” by David Lorell

LessWrong (30+ Karma)

“Redux: (∃ Stochastic Natural Latent) Implies (∃ Deterministic Natural Latent)” by David Lorell