The most important question about AI isn't whether it can think. It's that for the first time, invention costs nothing. All that's left to measure is intent.

This is my view of the world working on the trailer tonight for my second film Thirty-One Mirrors. I wrote the novel. Did adversarial testing of it. Then went book to script. Script to what you're seeing here. I was there where Adobe Premiere was born and Avid hit the world ... this is something different. I'm not worried about color-timing, audio, sfx, titles ... I'm just telling a story.

Every level in this game is a theorem. I built HeartGrid, a Lolo-style puzzle game: push emerald blocks, bridge the water, collect the hearts, dodge ghosts that patrol and hunt. Then I asked Lean 4 to prove things about it. For each of the 12 rooms, Lean proves: ✅ it can be solved ✅ it can’t be solved in fewer moves (the exact minimum) ✅ and across the set, the minimums strictly increase: 15 < 27 < 33 < 38 < 47 < 61 < 67 < 84 < 98 < 107 < 110 < 114 So the difficulty curve isn’t a designer’s hunch or a playtest average. It’s a statement a machine checked. To be clear: Lean is a serious tool. Mathematicians and engineers use it to verify real theorems and real software. This is the playful end of the same idea. But it shows something genuinely useful. Once the rules are written down precisely, “is this puzzle fair?”, “is it too easy?” and “does the next level actually get harder?” stop being opinions and become things you can check, for every level, again and again, even after you change the rules. How it works: random corridor mazes go to an exact solver; Lean re-checks every solution and proves the search itself is sound, so “no shorter solution exists” is a proof, not a claim. Honest footnote: the game you play is JavaScript, a second implementation of the rules that I keep in sync with tests rather than proof. And for 11 of the 12 rooms the exhaustive search runs as compiled code (native_decide), so that part also trusts Lean’s compiler. Play it, free, in your browser: keithadler.github.io/heartgr… Code and proofs (MIT): github.com/keithadler/heartg…

San Francisco’s whistleblower hotline is getting busier. Reports to the Controller’s Whistleblower Program jumped 31% in the second half of 2025, 398 vs 304 a year earlier. That’s the second-highest stretch in the program’s ten years. Full-year reports have doubled since 2015, from 325 to 661. These cover misuse of city funds, improper conduct by city employees, poor service and waste. A report isn’t proof of wrongdoing: about a third of investigated reports end in corrective action. But more people are raising their hand. Source: SF Controller’s Whistleblower Program updates, Aug 2025 and Feb 2026.

Claude I didn't ask for all this.

Heads up @DataSF: the Police Department Incident Reports dataset (wg3w-h783) looks like it lost most of its records in a reload. On October 7 it held 76,325 incidents for 2025 alone. Today the entire file, 2018 to 2026, is 58,057 records. 2025 is down to 4,299, and every year and crime type shrank the same way, including homicides (28 in 2025 down to 1). The last update was this morning at 9:56 and added only 22 rows. Anyone running SF crime numbers this week will badly undercount until it’s reloaded. @SolveSF, flagging it since you work with this data too. Easy to check: data.sf.gov/resource/wg3w-h7…(*)

Where does a Lean kernel spend its time? I re-checked Init (57,919 declarations) from scratch with three kernels I wrote, in Java, C# and Haskell, and profiled where the time goes. I expected universes to show up. They don’t. Universe levels. Reasoning about them is under 2% of checking time. Declarations with universe parameters cost the same per declaration as ones without: 0.34 ms with none, 0.36 with one, 0.27 with two, 0.33 with three or more. Universe polymorphism is not the slow part. Substitution. Rebuilding terms is 55% of checking, and building and sharing expression nodes is another 40% (the two overlap, because each counts everything it calls). Reading the export is a further 20% of wall time. Tenet’s own counters show the same shape: 21 million substitution calls visiting 387 million nodes on Init. One cheap finding. 98% of universe instantiations, the step that substitutes levels into a constant’s type or value, repeat an earlier one. Lean’s own C++ kernel recomputes them every time too. I tried caching them in two kernels: 10% faster in Java, and 6.6% fewer instructions in Lean’s C++ kernel. Real, but small, and the C++ version has to respect the lifetime of memory-mapped .olean files (my first attempt crashed on exactly that). Not worth the complexity, so I dropped it. Three kernels, same export, one worker. Instructions retired: 271 billion (Java), 515 billion (C#), 555 billion (Haskell). Peak memory: 2.4, 3.3 and 0.84 GB. All three accept all 57,919 declarations. Caveats. This is Init only. Mathlib’s universe-heavy areas, like category theory, could change the universe result. The detailed profile is the Java kernel. The cross-kernel numbers are one run each on a busy laptop, which is why I quote instructions and not seconds. The per-declaration figures are timers; the breakdown is sampling. The takeaway for anyone building a faster kernel: look at substitution, not levels. The fast checkers on the Lean Kernel Arena use normalization by evaluation, which never substitutes. Tenet doesn’t, on purpose, because its point is to decide exactly what Lean’s kernel decides. github.com/keithadler/tenet github.com/keithadler/tenet-… github.com/keithadler/tenet-…

I've open-sourced tenet-jvm: an independent Lean 4 kernel, written in Java. A kernel is the small program that decides whether a Lean proof is valid. Every theorem you trust rests on it. Lean's own is written in C++. The more independent implementations check the same proof, the fewer bugs can hide in all of them at once. So this is not a flag-planting exercise. I maintain it alongside Tenet (the C#/.NET kernel) and the rest of the Lean verification chain. How it works It reads the output of lean4export and re-checks every declaration from scratch. For inductive types it does not believe the export. It takes only the types and constructor types, derives the recursors, recursor rules and bookkeeping flags itself (nested and mutual inductives included), and rejects the file if anything differs. Derive, then compare. What it has checked, with every declaration accepted and nothing taken on trust • Init: 59,349 constants • Std: 99,619 • The whole Lean library: 171,705 constants, 2,860 inductive groups, in under a minute • con-leche, cedar and cslib from the Lean Kernel Arena: 27,959, 148,832 and 394,284 constants Why "verified" means something A kernel that accepted everything would print the same words. So: • 197 of 197 decided Lean Kernel Arena tests are correct locally, with none wrongly accepted and none wrongly rejected. That includes the soundness bugs that were found in real kernels. • Mutation tests corrupt a valid export 16 ways, and 6 more inputs that are not exports at all. All are rejected. • It fails closed. Testing found two of my own bugs: a crash that exited as "accepted", and an empty input accepted as a valid file. Both are fixed and now tested. Mathlib exposed more. It found a false rejection (a type hidden behind a definition) and a slowness bug (comparing arguments in the wrong order made one declaration take 10+ minutes; now 3 seconds). What it is not: formally verified. It is tested, which is evidence and not proof. The README has a section on exactly what you still have to trust, and docs/divergences.md lists every place it decides something differently from Lean's kernel. Java 21, no dependencies, Apache-2.0. make and you're running. Next: the Lean Kernel Arena submission. github.com/keithadler/tenet-… #Lean4 #FormalVerification #TheoremProving

Announcing tenet-hs: an independent Lean 4 kernel in Haskell. Free, open source, Apache 2.0. Lean is a functional language, and the kernel that decides whether a proof is correct is C++. This is an independent implementation of that kernel in another functional language. Expressions, universe levels and declarations are algebraic data types, and every typing, reduction and equality rule is a case over them. The docs list each rule next to the function that implements it, so you can read the code against the type theory. It reads lean4export files and re-checks every declaration from scratch. It re-derives every constructor and recursor, nested and mutual inductives included, and compares them with what the exporter wrote. It checks that Nat.add really is addition before taking the arithmetic shortcut, and it will not trust compiled code. What it has been run against: - All of Lean's Init: 57,919 declarations accepted, none rejected. - The same file with every theorem handed another theorem's proof: it rejects 41,378, and Tenet, my C# kernel, rejects the identical 41,378. - 350 randomly damaged files compared against Tenet: no disagreements. The first run of that fuzzer found a real bug in tenet-hs, 9 of 120 files, and it is fixed. - The Lean Kernel Arena's published test suite: 196 of 196. The honest parts. It is not purely functional: substitution and the caches use mutable tables, because persistent maps were 75% of the profile. I tried hash-consing, the functional favorite, and it was ten times slower on these inputs, so it went back out. It is two to five times slower than Tenet on the arena's performance tests, it is single-threaded, and I have not run Mathlib yet. The design notes have every profile and every dead end. It builds with the GHC you already have and needs no packages. I am not planting a flag. I will maintain it alongside Tenet and the rest of the family. The more independent kernels there are, the better: every one is another chance to find a bug in the reference kernel, in the others, or in the spec they are all trying to match. github.com/keithadler/tenet-… #lean4 #haskell #functionalprogramming #formalverification #opensource

Introducing leanout: a clean-room Lean 4 exporter, Apache-2.0. Written from the published format spec alone, with no other exporter’s source read. Exports of Init, Std, all of Lean and 338k constants of Mathlib are accepted by both Lean’s own kernel and Tenet. Zero failures. github.com/keithadler/leanou…

Just opened a PR to Microsoft’s LiteBox: the Linux seccomp policy is now data, not code. 🔒 Every syscall the runner may still make after the filter goes on is one row in a table. Each row has its argument conditions and the reason it’s needed. What it brings: 📋 Policy as a table. The compiled BPF is byte-for-byte identical on x86-64 and AArch64, debug and release. 👀 Reviewable. One-screen policy files, kept in sync by a test, so a change to the host interface shows up in review as a one-line diff. 🚫 No host path opens after the filter. CoW mappings now come from a descriptor registered up front, so open/openat are denied outright. Swapping the file on disk can no longer change what gets mapped. 🛠 clock_gettime fix for hosts where the vDSO can’t serve it (hpet VMs). test_seccomp_filter now passes there. Also: a duplicate syscall entry now panics instead of silently replacing the earlier one, and denial warnings say fcntl (25) instead of just 25. Tested on AArch64 (658/658) and x86-64 under QEMU (622/622). github.com/microsoft/litebox… #Rust #Seccomp #Sandboxing #OpenSource

Lean checks every proof. It doesn’t check that a lemma named _left is about the left, that a lemma ending in _iff is an iff, or that a docstring still points at something that exists. I built lean-linter to catch that. It reads a compiled Lean library and compares names with statements. On Mathlib and Lean core it found 2,183 things that weren’t already reported. A few examples: mono_iff_surjective states mono ↔ injective DFinsupp.coe_strictMono only proves Monotone, so the strict lemma doesn’t exist reflexivePair_map_left is about .right in Lean core, Std.Roc.lower_le_of_mem concludes a strict < Every proof is fine. This is cleanup, and plenty of the 2,183 don’t need fixing. But I’ve opened four Mathlib PRs for the clearest ones, and filed an issue on Lean core for three more. A Mathlib maintainer has already reviewed one. Open source, works on any Lean 4 project: github.com/keithadler/lean-l…

I ran the check the Navier-Stokes critique asks for on OpenAI's proof of Saxl's conjecture: does the Lean say what the paper says? For the statements, yes. The Lean headline matches Theorem 1.1 exactly: every m >= 1, every partition, no extra hypotheses. It proves the stronger cyclic Theorem 3.1 that the paper actually proves, with the same generator and the same thresholds (m >= 5 and at most four strips in case (ii)). No junk values found, and no sorry, axiom, native_decide or opaque in the 38 files. How, with Claude and my tools: - Lean built all 38 of OpenAI's modules at their exact pins. - Tenet, my independent kernel, re-checked 768,336 declarations in 10,782 modules, 0 failed. saxl_conjecture rests on propext, Classical.choice and Quot.sound only. - Lean Studio's verify: 600 of 600 declarations proved outright. None rest on sorry, project axioms or compiled code. - Claude read the 17-page paper and traced Sections 2 to 6 against the Lean in four parallel audits. I checked its key claims against the files myself. Where the paper says more than the Lean states: Pieri and Young's rule (the paper states iff and multiplicity one; the Lean has the positive direction only), Lemma 2.1 in general (the Lean: tableaux only), and Proposition 4.2 (the paper: a surjection onto the full induced module; the Lean: a nonzero map into W_m, and there is no induced module anywhere in the 38 files). Nothing in the Lean's proof needs the missing parts. But the Lean does not check those prose lemmas as written. That is the critique's point: a checked proof is not a checked paper. In several places the Lean also takes a different route to the same fact: the paper's (3.5), the Ryser margins, the eigenvector conjugation. My own formalization found independently that (3.5) is not needed. Context: I started formalizing this independently yesterday and re-derived about half of it before I noticed OpenAI's repo already had a complete Lean proof. The general pieces underneath became two Mathlib pull requests (#44612, #44613). OpenAI built the rails. Mathlib is the train station other people can use. Limits: I read statements, not proofs, and I make no claim about the mathematics. Everything is checkable. OpenAI's repo: github.com/openai/math My formalization: github.com/keithadler/saxl-l… Mathlib PRs: github.com/leanprover-commun… and /44613 Tenet: github.com/keithadler/tenet Lean Studio: github.com/keithadler/leanst…

Final update on my Saxl's conjecture formalisation. The headline, stated plainly: OpenAI's repo already contained a complete Lean proof of their own paper - 38 files, no sorry - pushed a few hours prio. I didn't expect to be first I really wanted to push throuh the tool chain of Tenet and Lean Studio towards a independent proof or optimization if one existed. What this effort actually produced: • An independent formalisation of about the first half of the paper (~8,000 lines, every theorem axiom-checked): Specht modules, James's submodule theorem, Pieri, the strip reduction, and a from-scratch proof that every irreducible representation of S_n is a Specht module. Saxl's conjecture verified independently for all partitions of 1, 3, 6 and 10. • The full statement is now closed in the repo too — by vendoring OpenAI's proof under its Apache licence and bridging it to the challenge file. The README has a provenance table saying exactly which theorems are mine and which are theirs. Nothing is passed off as more than it is. • Two Mathlib PRs (#44612, #44613) generalising the counting inputs to any finite group. Those were never in Mathlib and still aren't; they're under review. • One small finding: a step in the paper's Prop 3.2 (eq. 3.5) is unnecessary. Lesson, for anyone doing this kind of thing: before investing in "first to formalise X", read the formalization catalogue in the source repo yourself. Five minutes. I delegated that check and it came back wrong. The Mathlib PRs are the part that outlives this. Next project starts from a verified gap. Built with Claude assisting. github.com/keithadler/saxl-l…

Progress update on formalising OpenAI's "Cyclic Polytabloid Proof of Saxl's Conjecture" in Lean 4. The paper quietly assumes "every irreducible representation of S_n is a Specht module." Mathlib didn't have it, and without it the induction stalls at the small cases. It's now machine-checked in my repo — no Wedderburn–Artin, just character orthogonality plus counting. Two of the ingredients are general facts that were missing from Mathlib itself, so I opened PRs for them today: • #44613 — irreducible representations of a finite group are bounded by its number of conjugacy classes github.com/leanprover-commun… • #44612 — conjugacy classes of the symmetric group correspond to partitions github.com/leanprover-commun… I think I'm first to submit these: I checked master, open PRs and the Zulip archive, where the counting result has been listed as a gap since 2020. Where things stand: Saxl's conjecture is fully verified for staircases up to size 10, roughly 45% of the paper's proof is formalised, and what's left is the width-two band computation and the final assembly. Built with Claude assisting. Repo: github.com/keithadler/saxl-l…

Progress update on formalising OpenAI's "Cyclic Polytabloid Proof of Saxl's Conjecture" in Lean 4 / Mathlib. Milestone reached today: Saxl's conjecture is now machine-checked for the staircase partitions (1), (2,1), (3,2,1) and (4,3,2,1) - every irreducible representation of S_1, S_3, S_6 and S_10 is proved to appear in the corresponding tensor square. Stated against OpenAI's own challenge file, verbatim, with only Lean's three standard axioms. What's done: Specht modules + James's submodule theorem (irreducibility), Pieri via strip tableaux and Frobenius reciprocity, the paper's Lemma 4.1 "sector" trick, Prop 3.2, the horizontal-strip reduction, and Prop 4.2 in the width-one case. Then the paper's induction, which closes completely for m ≤ 4. Rough estimate: ~40% of the full proof. The main blocker for m ≥ 5: the paper quietly uses "every irreducible of S_n is a Specht module". Mathlib doesn't have that yet. Formalising it is the next sub-project as it'd be useful far beyond this paper. Side finding along the way: one step in the paper's Prop 3.2 (eq. 3.5) isn't needed - the machine-checked version goes through without it. I'll share that with the authors. Repo: github.com/keithadler/saxl-l…

Lean Studio: a native Lean 4 IDE. A second kernel, Tenet, re-checks every proof you build. Prove It tries 17 tactics on each sorry. Local AI whose proofs Lean checks first. 127 MB installed, vs 856 MB for VS Code alone. Free and open source: github.com/keithadler/leanst…

Cantor's diagonal argument, formalized in Lean 4 with Lean Studio. List binary sequences, one per row. Flip each bit on the diagonal. The new sequence differs from row n at position n, so it is on no row. There are more binary sequences than natural numbers. Lean checks every step, and Tenet re-checks it with an independent kernel. No Mathlib, and it depends on no axioms at all, not even propext. Code: github.com/keithadler/cantor… Lean Studio: github.com/keithadler/leanst…

Why are engineers involved with Math and talking Lean? Here's a great example ... A lot of what your computer trusts is signed in one format: CMS, the signature inside PKCS #7, S/MIME email, Windows Authenticode, PDF signatures, signed Linux kernel modules and trusted timestamps. I wrote down RFC 5652's signing rules in Lean, proved a verifier equal to them, and had Lean's kernel check real signatures, including a 4096-bit RSA timestamp from DigiCert. As far as I can find, nobody has formalized CMS before. Then I tested six widely used verifiers against it: OpenSSL, LibreSSL, GnuTLS, Java, .NET and Apple. Each test message had exactly one flaw and a valid signature. What I found: - OpenSSL, LibreSSL and .NET let anyone change what kind of content a signed message says it holds, with no key, and still call the signature valid - GnuTLS accepts one signature as valid for two different documents - given the same file, OpenSSL and GnuTLS can reach opposite verdicts on whether it is validly signed - .NET and Apple accept an RSA signature one byte too short - Java's signed-JAR verifier cannot read a signer named by key ID, which the standard requires None of these lets an outsider forge a signature, and I judged them low severity, so they are reported in public to OpenSSL, LibreSSL and .NET. MIT: github.com/keithadler/lean-p…

Billions of people use spreadsheets every day, and most XLSX files are read by code, not by Excel: bank exports, payroll, lab results, data pipelines. That code is mostly three open source readers: openpyxl (Python), calamine (Rust) and SheetJS (JavaScript). I wanted to know if they read XLSX correctly, so I wrote down what a valid XLSX file is, precisely enough for a computer to check, and tested the latest version of each against it: 382 hostile files, plus all 418 real test files from Apache POI and calamine. What I found: - openpyxl deletes every "x005F_" from shared-string text: the cell "ax005F_b" comes back as "ab" - openpyxl silently drops a sheet whose link is broken, and silently throws away values under merged cells - one bad hyperlink ID, comment author or conditional format makes openpyxl refuse the entire workbook - calamine reads a value written at cell A4294967297 back at A1, and a 1 KB file can make it try to allocate four billion columns - calamine and SheetJS open archives whose checksums fail and hand you the corrupted data without a word - put two copies of the same sheet in a file, and openpyxl and calamine read one while SheetJS reads the other - when a cell is written twice, all three silently keep the second value - "npm install xlsx" still gives you SheetJS 0.18.5, which reads early dates a day off and ignores the 1904 date system. The newer 0.20.3 fixes that but drops carriage returns from text - on Apple's built-in Python 3.9, one of Apache POI's XML bomb files makes openpyxl run until killed Some of these were already reported and are being fixed. I sent calamine a fix for one that wasn't: github.com/tafia/calamine/pu… The spec is written in Lean because it has to be right before it can judge anyone else. The checkers are proved sound, so when a file breaks a rule, the tool names the rule and the cell. Testing it caught my own mistakes too: rules stricter than the standard, and a writer bug that would have turned your text "_x0041_" into "A". Check your own files: xlsxlean check file.xlsx MIT: github.com/keithadler/xlsx-l…