I finally brought my repository up to date: sturm-liouville-comparator-run. It holds a formal, computer-checked proof of a classical result from Sturm–Liouville theory, written in the Lean 4 proof assistant. Here’s what that means, why I care about it after desk rejections and a Mathlib suspension, and what it does and doesn’t claim.
The problem
Take the one-dimensional Schrödinger equation, −u″ + V u = λ u, where V is a potential that is continuous and grows without bound as you go out to infinity in either direction. Physicists call this a confining potential. The harmonic oscillator is the textbook example.
The theorem says that for any energy λ, if you find two nonzero, square-integrable solutions, they must be multiples of each other. In plain terms, each energy level in a confining 1D potential has exactly one state, up to scaling. Mathematicians say the eigenvalues are simple, and physicists say there’s no degeneracy in 1D bound states.
Why it matters
This isn’t new mathematics. It’s about a century old, the limit-point case of Weyl’s theory, and it’s in standard textbooks like Coddington–Levinson and Teschl. But a lot of physics and spectral theory rests on it, and “everyone knows it” isn’t the same as “a machine has checked every step.”
I’ve worked on this since March, and when I searched as of November 3, 2026, I couldn’t find a completed Lean proof of this result. Mathlib had no Sturm–Liouville, Schrödinger, or function-Wronskian material that I could find, and the closest projects I saw either worked on a compact interval or left the proof as a placeholder. If someone has done it, I’d love to hear about it. Open an issue on the repo.
How the proof works
It follows the classical argument in four steps:
- The Wronskian of two solutions at the same λ is constant.
- A square-integrable solution of a confining equation goes to zero at infinity, and so does its derivative.
- So that constant Wronskian has to be zero.
- A zero Wronskian forces the two solutions to be linearly dependent, by uniqueness of solutions to the initial-value problem.
The proof file has 3 definitions and 14 lemmas and theorems, with no sorry (Lean’s placeholder for “trust me”).
What the run shows
The same file was checked three ways:
- Axiom audit. The theorem depends only on Lean’s three standard axioms (propext, Classical.choice, Quot.sound). It uses no custom axioms and no shortcuts.
- Comparator, Nov 3, 2026. Comparator is the Lean FRO’s proof judge. It confirms that the proved statements match the challenge statements exactly, including every definition they rely on, then replays the proofs through the kernel. It returned “Your solution is okay!” with Lean’s kernel. A second run with NanoDa, an independent kernel, accepted it too. The full log is in the repo.
- Comparator, cold and sandboxed, Oct 29, 2026. The same four theorems were judged in a larger sandboxed run with every input hashed. The verdict was ACCEPTED, and the receipt is in my companion receipts repo.
Everything is pinned to Lean v4.34.1 and a fixed Mathlib commit, so anyone on Linux can rerun the build, the audit, and Comparator using the steps in the README.
How it was built
I did this with AI the whole way, under my direction. An AI proof-search tool produced the original proof in three variants back in March. In October I consolidated them into one clean file, keeping only the lemmas the variants share and dropping the dead ends. Then, with an AI coding assistant, I ported it to the current Lean and Mathlib versions. That took fourteen mechanical changes inside proofs, and no definitions or statements changed. The repo’s provenance section has the full details and credits.
Limitations, honestly
- The math is classical. What’s new is the formal, machine-checked version, not the theorem.
- The statement covers classical square-integrable solutions on the real line. It doesn’t build a self-adjoint operator or its domain.
- The Nov 3 Comparator run happened on my laptop with a prebuilt library, outside the stricter sandbox. The Oct 29 run is the cold, sandboxed one.
- “No Lean proof known” just means I searched and didn’t find one. It isn’t a priority claim.
This theorem also feeds into a larger Lean library I’m building, where it serves as the Schrödinger-side input. More on that when it’s ready.
Repo (Apache-2.0): github.com/Joeyxyxyz/sturm-liouville-comparator-run
Leave a Reply