LaurieWired (verified) @lauriewired · 2h
The boom in Linux CVEs lately should get you thinking.
Surely, given a finite codebase, there are also a finite number of bugs / unintended behavior, thus, a finite amount of vulnerabilities. Theoretically, a "solvable" problem. Right?
Well...not at all actually.
It gets a bit philosophical, but there's the concept of "weird machines".
A weird machine is an accidental computer located inside of another computer program. Quite a few exploits (e.g. anything ROP) falls into this category, where the attacker's instruction set consists of fragments of the original software.
Finite code can *easily* have infinite Unintended Behavior (not undefined behavior btw...that's a very different thing). Weird machines don't even have to be Turing complete to be, really, really powerful!
Even if you have a million superhuman AI coders and fuzzers thrown at the Linux kernel, you quickly hit halting-problem-esque uncomputable states. The concept of patching every possible bug until none remain isn't possible, because we can't often correctly define what a "bug" even is.
Now, can you make a kernel that truly has zero weird machines relative to a formal specification? ....yes, but it wouldn't look like Linux. It'd look more like sel4, VxWorks, or (shudder) INTEGRITY-178.
Note from Claude Sonnet 5
Long tweet arguing that a finite codebase can have unboundedly many unintended behaviours (weird machines), so patching Linux until no bugs remain is not achievable even with vast numbers of superhuman AI coders and fuzzers; conceptual, no exploit specifics.
Thomas Ahle @thomasahle · Sep 11
Compute Polynomials Twice as Fast -
Here's a fun result, done entirely without AI.
That because we proved it years ago, but it ran a hundred pages and we weren't quite sure enough to publish. Now AI verified it in Lean.
A fun fact about polynomials is that
P(x) = x⁴ + a₃x³ + a₂x² + a₁x + a₀
can be evaluated in just two(!) multiplications!
The trick is to write
y = (x + b₀)x + b₁
P(x) = (y + x + b₂)y + b₃
where b₀...b₃ are easy to calculate from a₀...a₃.
Polynomials are everywhere from computing exp/sin, to cryptographic hashes and codes. Over finite fields multiplications are particularly expensive, so a 2x speedup matters.
Donald Knuth and others showed ~n/2 multiplications suffice for any degree n, but their preprocessing needs complex roots: numerically unstable and useless over finite fields. Rabin & Winograd fixed that with rational preprocessing, but 2logn extra multiplications, which hurts at the small n we most care about.
Our new method solves this. It uses ⌈(n+1)/2⌉ multiplications, and we prove this is optimal.
You can try it out on your own polynomials at
thomashale.com/fast-polynomia… [cut off]
Note from Claude Sonnet 5
Long X post by Thomas Ahle announcing a result on evaluating polynomials with roughly half as many multiplications (ceil((n+1)/2), proven optimal), with a worked quartic example; says the proof was long and was only now verified in Lean by AI.
Brendan Dolan-Gavitt [verified] @moyix · 58m
Working with frontier LLMs for vulnerability research lately has made me feel like I woke up one day and found the solid walls of my house were all made of paper. I knew humans were not good at secure software but having fistfuls of Chrome vulnerabilities makes it very real
[6 replies, 2 reposts, 58 likes, 1.4K views]
Justin Halford [verified] @Justin_Halford_ · 27m
It seems like a fair conclusion that we will need to rebuild virtually all software so that is formally verified end to end. It makes me wonder if there are bugs implicit to the stack between the machine language and our high level languages, even as deep as the hardware itself.
[3 replies, 5 likes, 56 views]
Brendan Dolan-Gavitt [verified] @moyix · 23m
I had a sort of depressing chat with GPT the other night where I asked if we ever fixed all those cache side channel attacks people wrote about in the mid-2010s, and it was like "no we decided to live with them instead"
Note from Claude Sonnet 5
Dark-mode X screenshot of a three-post thread: Brendan Dolan-Gavitt (@moyix) on frontier LLMs making software insecurity feel very real, Justin Halford replying that software may need to be rebuilt as formally verified, and moyix adding an anecdote about a GPT chat on unfixed cache side-channel attacks.
Costa @Clambr0 [Follow]
hello Erdős asked if Σ n!/(2n)! is irrational
It is. Five-line proof. Extends to the whole family Σ n!/((a+1)n+b)! for a≥1, 0≤b≤a. Lean verified.
My AI then went crazy and claimed the whole affine family a≥1, b≥1-a is transcendental using techniques beyond my understanding:
[link card]
clambro/erdos-270-transcendence
Transcendence in the Affine Case of Erdős Problem 270
1 contributor · 0 issues · 0 stars · 0 forks
GitHub - clambro/erdos-270-transcendence: Transcendenc...
From github.com
2:26 PM · Aug 22, 2026 · 71.2K Views
10 replies · 30 reposts · 465 likes · 193 bookmarks
Relevant ▾ View quotes >
[next post in thread]
Costa @Clambr0 · Aug 22
[embedded image of typeset math, bottom partly covered by phone nav bar]
Let
C = Σ_{n=1}^∞ n!/(2n)! = Σ_{n=1}^∞ 1/D_n, D_n := (2n)!/n!.
Since
D_{n+1}/D_n = 4n + 2 ∈ ℤ,
we have D_n | D_{n+1}.
Let P_N = Σ_{n≤N} 1/D_n and R_N = C − P_N. Then D_N P_N ∈ ℤ, while
0 < D_N R_N ≤ Σ_{k≥1} 1/(4N+2)^k = 1/(4N+1) → 0.
Note from Claude Sonnet 5
Tweet by Costa (@Clambr0) saying a five-line, Lean-verified proof shows the Erdős-asked series sum of n!/(2n)! is irrational (extended to a family), and that his AI then claimed transcendence for a wider affine family, linking a GitHub repo for Erdős Problem 270; below, the start of the thread with the typeset irrationality proof. Posted 2026-08-22.
[top of screen, cut off: end of the previous post]
@OpenAI!
1:52 PM · Aug 24, 2026 · 9,825 Views
4 replies · 9 reposts · 113 likes · 25 bookmarks
Relevant ▾
Grigore Rosu @RosuGrigore · 4h
Matching logic is complete without μ, incomplete with μ!
In passing, we also solved two open problems in hybrid logic: the nominal-free fragment is complete; with nominals only, incomplete. This is surprising because if we add pointed validity it becomes complete again (known from 2006).
[embedded diagram of logics and completeness results: the same diagram as in the previous capture, Screenshot_20260824-181724.png; node labels not repeated here]
1 reply · 1 repost · 17 likes · 1.4K views
Grigore Rosu @RosuGrigore · 4h
Here is the paper. Comments are welcome.
arxiv.org/pdf/2608.13306…
Why is matching logic interesting at all? Pure type systems, dependent types, calculus of inductive constructions, etc., MSOL, SOL, HOL, etc., can be defined as matching logic theories. That is, Lean, Rock, Isabelle, etc., proofs can be mechanically translated to matching logic, which is a simpler logic (so it admits a smaller proof checker).
Note from Claude Sonnet 5
Scrolled continuation of the Rosu thread from seq 9: the matching-logic completeness result with the diagram, then a third post linking the paper (arXiv 2608.13306) and explaining why matching logic matters for proof-checker size. Bottom of the capture is overlaid by phone UI (nav bar, compose button) that overlaps a few lines.
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.
