Researcher in maths+formal methods+ml. Using formal verification to train models for mathematics, software, hardware, general reasoning @harmonicmath
London, UK
Joined May 2010
- Tweets125
- Following3.6K
- Followers633
- Likes140
Alex J Best retweeted
Aristotle can now formally verify Verilog and C!
On @TensordyneInc's most complex block, with 12.2M gate equivalents, 1.24M flops and hundreds of state machines running concurrently, it proved 185 whole-block properties and found bugs up to 110,000 cycles deep.
Alex J Best retweeted
Tensordyne gave Aristotle its hardest block to verify: 12.2 million gate equivalents. 185 properties proved, 56 refuted.
Jonathan Ko, their verification engineer, calls it "unthinkable with traditional tools."
Read the the full @TensordyneInc case study: harmonic.fun/aristotle/case-…
Alex J Best retweeted
oh my. pointed aristitle at TorchLean's C runtime code and in ~6 hours: 211 of 213 properties proved (memory safety, refcounts, functional correctness)
The other two came with a use-after-free counterexample involving inconsistent caller reference counts. We are reviewing the ownership assumptions and proof artifacts to establish exactly what’s guaranteed: ) im very impressed!
Alex J Best retweeted
If you can verify math, you can verify code. And hardware. And pretty much any system you can model!
"US fusion lab DIII-D said Aristotle rebuilt part of its reactor-control software in four hours from one research paper and a 254-word prompt."
reuters.com/technology/robin…
We've been working on verifying software and hardware, so that we can eliminate bugs in the most important parts of the technology stack, and let models autonomously iterate without compromising on correctness. I'm super excited we can now make this technology available to all!
Alex J Best retweeted
Fast inference and verified answers go well together. Tudor (@tachim) is on the Neo Labs panel at the SGLang Summit with Igor Babuschkin, Eric Zelikman and Liam Fedus, Nov 12–13 in SF. Don't miss this one.
Proud to welcome our newest sponsors to SGLang Summit.
In just one week since our public announcement, our sponsor lineup has grown from 11 to 36. Thank you to every sponsor helping bring this community together.
Join 2,000+ engineers, researchers, and builders from across the AI ecosystem for technical sessions, hands-on workshops, and the GPU Expo.
Hear from Lip-Bu Tan, Lilian Weng, Soumith Chintala, Aravind Srinivas, and more. Meet the teams building across AI hardware, infrastructure, models, and applications.
🗓️ November 12–13, 2026
🌉 Fort Mason, San Francisco
🎟️ Get your tickets: sglang.io/summit
Alex J Best retweeted
I mentioned Gödel and Escher during my talk at REBASE 2026 but I could not fit in Bach. conf.researchr.org/details/s…
Alex J Best retweeted
@HarmonicMath is hiring a Formal Verification Engineer to develop Aristotle and apply it to formally verify production hardware and software!
The work spans formal methods research, product development and customer deployments.
Join our team in Palo Alto or London!
🔗 jobs.ashbyhq.com/Harmonic/5e…
Alex J Best retweeted
Leonardo Franchi, Fredy Yip and I recently solved a problem of Ben Green by showing that if A is an open product-free subset of the open interval (0,1), then A has measure less than 1/3, a bound that it is not too hard to prove is sharp. 🧵
Alex J Best retweeted
Today @HarmonicMath published solutions to eight previously studied open problems, solved autonomously with the help of Lean: arxiv.org/abs/2607.17477
And -- importantly! -- the paper and code show the whole "development" process, from initial proof to cleanup to exposition.
Alex J Best retweeted
I consider myself a relative newcomer to AI (started in early 2024), but I go back far enough to have worked on GSM8k and MATH. This is a sample of problems, all solved by AI, from various benchmarks since then. It's mind-boggling how quickly they've advanced. I expect a transformative year ahead.
🤖 Made with AI
Alex J Best retweeted
Oh and Kim Morrison used Claude + Aristotle + Codex to formalize the negation of the Erdos unit distance conjecture: github.com/kim-em/erdos-unit…
It's nice to see that this was built on top of PNT+; so despite the fact that we haven't been able to upstream it to Mathlib (the Residue Theorem we have in PNT+ is just for rectangles, and Mathlib will want a much more general version...), it's still useful in other applications!...
Two big autoformalization projects announced today!
One is @scottnarmstrong's (see below) formalizing his 2025 Inventiones PDE paper. Congrats Scott!!
Another is Buzzard's Jacobian Challenge, which @radokirov, Michael Douglas, Michal Wallace, Jack McCarthy, and others announced on zulip.
So we're in the realm of possibility for moderately difficult automatic formalization! Still no autoformalization of all of FLT, nor Zaremba; but much evidence points in that direction...
The next order challenge is auto-cannonization: we only get the positive feedback loop of people being able to build reliably on top of these projects, if they're fixed up, "cannonized", and PR'ed to Mathlib. The maintainers are capable of that task; we need AI that can help speed up their workflow!
Alex J Best retweeted
I used @HarmonicMath's Aristotle to formalize Erdős problem #426 in Lean 4…
and ended up fully verifying a stronger bound that the original paper only suggested 🧵
Erdős offered $25 for a disproof, and $100 if the conjecture was true 👇
Alex J Best retweeted
"Aristotle's proof is correct, simple, elegant, and beautiful. It uses techniques in the original paper and adds its own new ideas. I am amazed and impressed by what Aristotle has done."
This is what Melvyn Nathanson, a leading additive number theorist and longtime Erdős collaborator, wrote to me after reading solutions by Aristotle (@HarmonicMath) to two problems he had posed earlier this year.
Our paper answers Nathanson's Problems 10 and 11 on product intersection sets in semigroups, and also settles the second parts of Problems 4 and 7 as corollaries.
Alex J Best retweeted
Kind of crazy. I had a rough idea for an Erdős problem, gave it to GPT-5.4 Pro, went for a walk, came back to a solution. I verified it, formalized it with Aristotle from @HarmonicMath together with @Tomodovodoo. Incredible how powerful these tools are in the right hands!
Alex J Best retweeted
No amount of testing will ever prove your software is secure. People are waking up to this. Formal verification isn’t academic anymore, it’s inevitable.
Introducing Project Glasswing: an urgent initiative to help secure the world’s most critical software.
It’s powered by our newest frontier model, Claude Mythos Preview, which can find software vulnerabilities better than all but the most skilled humans.
anthropic.com/glasswing
Another very cool use case of Aristotle in arxiv.org/abs/2603.28636, fixing a gap in GPT-5.4's proof. This is exactly why we need verification in the age of LLM produced mathematics; as LLMs get more reliable and more convincing we will increasingly use them for harder and harder tasks, and in domains like mathematics where correctness is key we need ways of verifying (and in this case repairing) that can keep up.
Alex J Best retweeted
A decade ago, I abandoned the first math problem my PhD advisor ever gave me.
This week, I finally solved it—and formally verified it—using @AnthropicAI's Claude Code, @OpenAI's Codex, and @HarmonicMath's Aristotle.
Here’s how AI turned my 10-year-old notes into a 15,000-line Lean 4 proof. 🧵
Alex J Best retweeted
"Lean in my view is the best programming language ever created." 😍
Great interview with @tachim and @vladtenev on @CogRev_Podcast!
🔗youtube.com/watch?v=-01-McQQ…
Alex J Best retweeted
I wrote an essay on proof assistants in the age of AI.
leodemoura.github.io/blog/20…