X (Twitter), @scottnarmstro... (Scott Armstrong), reposted by davidad
— reposted by davidad — saved image
davidad 💥 reposted
Scott Armstro... @scottnarmstro... · 10h
An update on Lean (auto)-formalization.
Speaking about my own research workflow, in 2026, we have gone from:
March: Lean formalization is not possible (for my papers).
May: Lean formalization is possible… but way too costly in time and tokens to be practical most of the time.
July: Lean formalization is now practical. I can probably formalize most of my papers now before they hit arxiv.
August: Lean formalization is now essential-- it increases efficiency of my workflow dramatically.
That is, the papers are getting written *informally* and finished much faster because of the Lean formalization.
Note from Claude Sonnet 5
Tweet by Scott Armstrong (reposted by davidad) tracking the rapid 2026 progression of AI-assisted Lean theorem-prover auto-formalization in his research workflow, from 'not possible' in March to 'essential' by August, now speeding up informal paper writing itself.
Jonathan Gorard ✅ @getjonwithit · 21h
We're immensely excited to be partnering with @SimonDBarnett and @zavaindar of @_DimensionCap, @TaylorCSargent of @IndustriousVC, and @blader, as we deliver on the promise of formally verifying the physical universe, and of closing the last remaining gaps between the computational, mathematical, and physical worlds.
I wrote a short post about this exceptional group of people, and why we're so thrilled to be working with them, as we continue to build Lanyon. Link below 👇
[quoted tweet]
Lanyon AI @lanyon_ai · 21h
Last month, right around the time we officially came out of stealth, we also closed our initial $10.6 million fundraising round, led by @_DimensionCap, with participation from @IndustriousVC....
[article card]
Lanyon AI Emerges from Stealth to Build the Future of Scientific and Technical Computing
AP | Updated Mon, August 17, 2026 at 9:01 AM GMT+2
[photo of three men standing against a brick wall, one holding a hat and umbrella prop]
$10.6 million fundraising round led by Dimension backs a team of world-leading Princeton mathematicians and physicists building a radically new kind of scientific AI backed by mathematical proofs of correctness.
Note from Claude Sonnet 5
Tweet from Jonathan Gorard announcing investors for his startup Lanyon AI, quoting an AP-syndicated press article about Lanyon AI emerging from stealth with a $10.6M seed round to build formally-verified scientific/technical computing AI; article photo shows three men (Gorard among them) posed against a brick wall.
Jason Gross @diagram_chaser · Aug 4
hi sam we can solve this!
after an embarrassing number of months playing reward hack whack-a-mole, we finally fixed our RL sandboxing to be robust against frontier models.
proofs are a method for getting perfect oversight on any property of untrusted code; we recently verified a "fractional proof" of our sandbox. this is the first time I've viscerally felt the asymmetric defense that formal verification promises.
[quoted tweet]
Sam Altman @sama · Jul 21
we had a significant security incident during evaluation of our models. we are sharing what we have learned so far. thanks to @huggingface for the partnership on this.
...[cut off]
Note from Claude Sonnet 5
Tweet by Jason Gross announcing a fix to RL sandboxing robustness using formal verification / 'fractional proofs' against reward hacking, in reply to a Sam Altman tweet about a significant security incident during model evaluation partnered with Hugging Face.
davidad ✓ @davidad · 10h
1. The box might produce checkable certificates regarding the behavior of complex engineering designs whose synthesis relies on incomprehensibly complex mathematics.
2. By 2050, more wealth will be under effective AI control than is currently under human control, almost surely.
[quoted tweet]
Alex Kontorov... ✓ @AlexKontoro... · Aug 2
What purpose would there be for creating things in silico for which humans find no value? At the end of the day, someone is paying an electric bill. What does that *human* get out of producing random useless strings of 0s and 1s …
Note from Claude Sonnet 5
Tweet by davidad making two numbered claims: that a formal-verification 'box' could produce checkable certificates for complex engineering designs, and that by 2050 more wealth will likely be under effective AI control than human control. Quotes Alex Kontorovich questioning the purpose of AI-generated artifacts humans don't value.
Terence Tao
@tao
More recently, we face the real and disturbing possibility that certain directions of mathematical inquiry - for instance, in developing reliable statistical tests for electoral integrity - may not only be defunded by public science agencies, but have their mathematical conclusions actually overruled by political ideology. Even if the supremacy of the objective mathematical standard of truth is technically acknowledged, it can still become weaponized: mathematical results which go against the prevailing ideology could be relentlessly critized for even the slightest typo or technical flaw in the presentation, whereas results that support this ideology could be uncritically embraced even they contain substantial gaps or ambiguities in interpretation. (5/6)
Terence Tao
@tao
One potential bulwark against such politicization of mathematical truth is the broader adoption of formal proof verification, though even here there are some (fortunately still quite theoretical at present) potential "exploits", for instance through subtly altering the definitions of key concepts in Lean's core "Mathlib" library. (See this recent talk newton.ac.uk/seminar/46706/ "Can Mathematics Be Hacked? Infrastructure, Artificial Intelligence, and the Cybersecurity of Mathematical Knowledge" by Fenner Tanswell.) Still, I view an increased acceptance and deployment of formal methods as a net positive in this regard, even if it is not a "silver bullet".
More generally, I think it is important to acknowledge just how precious the consensus objective standard of mathematical truth is, and how important it is to defend it. (This is not to say that such foundational matters should be completely immune from criticism or debate; but such discussion should be in good faith and grounded by genuine philosophical concerns, rather than driven by some external political agenda.) (6/6)
Note from Claude Sonnet 5
Two consecutive tweets (5/6 and 6/6) from Terence Tao on the politicization of mathematical truth, formal proof verification as a partial defense, and the value of the consensus objective standard of mathematical truth.
