Pinned Tweet
Today we’re bringing Aristotle to software and hardware!
Describe the properties your code must satisfy and Aristotle formally verifies that it meets them.
I’ve spent the past few months helping Aristotle expand from proving math to verifying code. I’m excited to see it available to everyone today.
Try it: aristotle.harmonic.fun
Describe the properties your code must satisfy and Aristotle formally verifies that it meets them.
I’ve spent the past few months helping Aristotle expand from proving math to verifying code. I’m excited to see it available to everyone today.
Try it: aristotle.harmonic.fun
We’re bringing Aristotle to code.
AI is writing more code than anyone can review. We're building the AI that verifies it.
Starting today with C and Verilog.
3
4
51
2,200
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.
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.
2
9
44
1,502
In a second project, Aristotle wrote a common sub-block from spec and proved all 37 properties it derived.
Using Tensordyne's synthesis reports, it then optimised the RTL and re-proved all 37: about 26% less power and 19% less cell area in an early iteration.
Using Tensordyne's synthesis reports, it then optimised the RTL and re-proved all 37: about 26% less power and 19% less cell area in an early iteration.
1
2
7
234
It’s been a real pleasure working with Jonathan Ko and the Tensordyne team on both projects.
You can read the full case study here: harmonic.fun/aristotle/case…
You can read the full case study here: harmonic.fun/aristotle/case…
0
1
4
100
A pleasure to help @wtgowers and his colleagues get their preprint formalised with Aristotle (@HarmonicMath).
The long case analysis that a referee would understandably prefer not to check by hand is now formally verified in @leanprover.
The code should be available on @github before long. After some further cleanup, parts of the supporting API may also be suitable for upstreaming to Mathlib.
The long case analysis that a referee would understandably prefer not to check by hand is now formally verified in @leanprover.
The code should be available on @github before long. After some further cleanup, parts of the supporting API may also be suitable for upstreaming to Mathlib.
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. 🧵
11
14
99
221,845
Here's what András Sárközy, Erdős's most prolific collaborator, asked 25 years ago:
"How small can one make the maximal gap between the consecutive elements of a multiplicative Sidon set selected from {1, 2, ..., n}?"
In particular: does there exist a multiplicative Sidon set A t every sub-interval of [1, n] of length at least √n contains at least one element of A?
The answer is yes. The solution was autonomously discovered and formally verified in #Lean by Aristotle. We then improved the bound below √n and Aristotle formalised our proof too.
"How small can one make the maximal gap between the consecutive elements of a multiplicative Sidon set selected from {1, 2, ..., n}?"
In particular: does there exist a multiplicative Sidon set A t every sub-interval of [1, n] of length at least √n contains at least one element of A?
The answer is yes. The solution was autonomously discovered and formally verified in #Lean by Aristotle. We then improved the bound below √n and Aristotle formalised our proof too.
4
23
124
60,167
A multiplicative Sidon set is a set whose pairwise products ab are distinct up to ordering, the primes being the canonical example.
Aristotle realised that the answer is affirmative by taking all integers congruent to 1 mod q, where q is the floor of √n and proved that this indeed gives a multiplicative Sidon set, which is a priori not at all obvious.
We then pushed the bound below √n. With ρ := (13 − √69) / 10 < 0.47, we prove that the interval length √n can be brought down to n^α for any α > ρ and all sufficiently large n.
• Preprint: arxiv.org/abs/2605.02064
• Aristotle: aristotle.harmonic.fun
Aristotle realised that the answer is affirmative by taking all integers congruent to 1 mod q, where q is the floor of √n and proved that this indeed gives a multiplicative Sidon set, which is a priori not at all obvious.
We then pushed the bound below √n. With ρ := (13 − √69) / 10 < 0.47, we prove that the interval length √n can be brought down to n^α for any α > ρ and all sufficiently large n.
• Preprint: arxiv.org/abs/2605.02064
• Aristotle: aristotle.harmonic.fun
3
1
20
1,964
Nathanson has just published the recording of his talk about Aristotle’s solutions and it is very interesting to watch!
“I tried to figure out what it did that I didn’t do to solve the problems.”
“The incredibly clever idea that Aristotle had was…”
youtu.be/VBIxv-6m7sk
“I tried to figure out what it did that I didn’t do to solve the problems.”
“The incredibly clever idea that Aristotle had was…”
youtu.be/VBIxv-6m7sk
Interesting update: a few days ago, Nathanson presented a talk at the New York Number Theory Seminar explaining how Aristotle solved some of his problems.
2
16
53
10,411
Interesting update: a few days ago, Nathanson presented a talk at the New York Number Theory Seminar explaining how Aristotle solved some of his problems.
"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 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.
1
11
50
50,572
"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 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.
This is what Melvyn Nathanson, a leading additive number theorist and longtime Erdős 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.
8
29
164
38,009
To my mind, what seems most important here is not so much the results themselves, nor even the particular methods used in the proof.
What really matters is the workflow: the closed loop from autonomous discovery of the right constructions, to formal verification of the proof in Lean, to informalised exposition back into a manuscript that mathematicians can read, understand, rewrite, and improve.
It suggests a framework in which formal proof is not merely a static final certificate, but an active part of mathematical research: a medium through which ideas are found, organised, tested, explained and made available for human judgment.
That dynamic loop is the real story for me. The natural next question is how far it can be pushed.
What really matters is the workflow: the closed loop from autonomous discovery of the right constructions, to formal verification of the proof in Lean, to informalised exposition back into a manuscript that mathematicians can read, understand, rewrite, and improve.
It suggests a framework in which formal proof is not merely a static final certificate, but an active part of mathematical research: a medium through which ideas are found, organised, tested, explained and made available for human judgment.
That dynamic loop is the real story for me. The natural next question is how far it can be pushed.
5
2
37
8,925
AI is increasingly changing how we do mathematics.
Erdős Problem #650, open for over 60 years, was solved a few weeks ago through a collaboration between human mathematicians, an informal reasoning model (GPT 5.4 Pro @OpenAI) and a formal one (Aristotle @HarmonicMath). 🧵
Erdős Problem #650, open for over 60 years, was solved a few weeks ago through a collaboration between human mathematicians, an informal reasoning model (GPT 5.4 Pro @OpenAI) and a formal one (Aristotle @HarmonicMath). 🧵
11
86
386
143,901
A thread like this one can only scratch the surface, but if you'd like to dive deeper, here are the two main references:
1. Informal @arxiv preprint: arxiv.org/abs/2603.28636
2. Formal @leanprover script: live.lean-lang.org/#project=mathl…
1. Informal @arxiv preprint: arxiv.org/abs/2603.28636
2. Formal @leanprover script: live.lean-lang.org/#project=mathl…
1
5
51
4,816
I also tend to see this story as a nice, concrete instance of @davidbessis's "System 3": the productive friction between informal intuition and formal rigour, except externalised across AI models rather than confined to a single mathematician's mind. davidbessis.substack.com/p/thinking-fas…
2
3
38
3,123