Share this page!

Enter URL or ID to Unroll

You can paste full URL like: https://x.com/threadreaderapp/status/1644127596119195649
or just the ID like: 1644127596119195649

How to get URL link on X (Twitter) App

  1. On the Twitter thread, click on or icon on the bottom
  2. Click again on or Share Via icon
  3. Click on Copy Link to Tweet
  4. Paste it above and click "Unroll Thread"!
  5. More info at Twitter Help
Harmonic Profile picture
@HarmonicMath
Mar 17 • 2 tweets • 1 min read • Read on X
🦾Meet Aristotle Agent, the world’s first autonomous mathematician — live and currently free of charge. We designed Aristotle Agent to solve and formalize the world’s most challenging mathematical research problems. It is now:

☑️#1 in Formal Math: We’re the #1 formal math model according to ProofBench, by @ValsAI, ahead of the closest competitor by 15%. Aristotle Agent can autonomously prove/formalize for up to 24 hrs without human intervention.
☑️Fully Agentic: Give it an English problem and it will prove/formalize from scratch, or it can work and edit files directly inside your Lean project / repository.
☑️Github-ready: Aristotle agent produces repo-quality code; project leads are increasingly merging Aristotle-drafted PRs with no modifications.

Now live across both web, CLI, and API. 🔥Image
Try it out at !aristotle.harmonic.fun

• • •

Missing some Tweet in this thread? You can try to force a refresh
　

Keep Current with Harmonic

Harmonic Profile picture

Stay in touch and get notified when new unrolls are available from this author!

Read all threads

This Thread may be Removed Anytime!

PDF

Twitter may remove this content at anytime! Save it as PDF for later use!

Try unrolling a thread yourself!

how to unroll video
  1. Follow @ThreadReaderApp to mention us!

  2. From a Twitter thread mention us with a keyword "unroll"
@threadreaderapp unroll

Practice here first or read more on our help page!

More from @HarmonicMath

Harmonic Profile picture
Nov 30, 2025
Many of us intuitively feel that the field of mathematics is going to change, so let's unpack the likely outcomes, without resorting to hyperbole or doomerism.
Hypothesis #1: The number of mathematical proofs and the aggregate amount of mathematical data will expand exponentially.

This one is perhaps uncontroversial. AI models, under the direction of humans, are already creating voluminous amounts of math. Now the bottleneck has gone from creating mathematics to verifying its correctness.

Aristotle, which uses @leanprover, solves the verification problem by enabling each proof to be machine-checkable.

As the technology improves, the length and complexity of the created proofs will continue to increase.
Hypothesis #2. There will be dramatically more mathematicians in 10 years than there are today.

By automating the drudgery of verification and proving simple lemmas, Aristotle can not only speed up the work of highly sophisticated professional mathematicians, but also lower the barrier to entry for others to contribute. Among our beta API users are retired software engineers, lawyers, military members, students, and plenty of other people that have mathematical ideas / ingenuity but need help with the formalism and need someone to verify their ideas. We should expect these trends to accelerate.
Read 5 tweets

Did Thread Reader help you today?

Support us! We are indie developers!

This site is made by just two indie developers on a laptop doing marketing, support and development! Read more about the story.

Become a Premium Member ($3/month or $30/year) and get exclusive features!

Become Premium

Don't want to be a Premium member but still want to support us?

Make a small donation by buying us coffee ($5) or help with server cost ($10)

Donate via Paypal

Or Donate anonymously using crypto!

Ethereum

0xfe58350B80634f60Fa6Dc149a72b4DFbc17D341E copy

Bitcoin

3ATGMxNzCUFzxpMCHL5sWSt4DVtS8UqXpi copy

Thank you for your support!

Follow Us!

Send Email!

:(