How I use Aristotle

Stream: PrimeNumberTheorem+

[Pietro Monticone]

Several people have asked me how I use Aristotle to contribute to the PNT+ / IEANT project so I'm writing this post with two goals in mind:

1. To describe the workflow I have developed and made publicly available.
2. To invite contributors to use it and help me maintain it.

Problem

The PrimeNumberTheoremAnd repository tracks the latest Lean and Mathlib releases (currently v4.28.0-rc1, but I'll bump it soon I'm afraid :sweat_smile:) and depends on several packages (e.g. LeanArchitect and LeanCert) that are not available in the Lean version currently supported by Aristotle (v4.24.0).

This means that, at the moment, you cannot simply point Aristotle at a file from the project repo and expect it to just work. The file needs to be converted into a format that is both compatible with v4.24.0 and optimised for Aristotle to make it as likely as possible that Aristotle can prove the theorem.

Workaround

I maintain a dedicated aristotle branch on my fork. This branch:

• Pins Mathlib to v4.24.0, the version supported by Aristotle.
• Simplifies lakefile.toml
• Is synced with upstream/main when I find the time to do so (help needed here!)

For every source file Foo.lean, the branch contains a corresponding FooAristotle.lean that has been converted for Aristotle.

Workflow

The workflow consists of two steps: convert and submit.

1. Convert

Run the conversion script on any source file:

scripts/convert_to_aristotle.py PrimeNumberTheoremAnd/CH2.lean

This produces PrimeNumberTheoremAnd/CH2Aristotle.lean. The script performs the following transformations:

1. Replaces specific Mathlib.Foo imports with import Mathlib and converts project-internal imports to their Aristotle equivalents (e.g., PrimeNumberTheoremAnd.Wiener becomes PrimeNumberTheoremAnd.WienerAristotle).

2. Converts blueprint_comment blocks to standard module docstrings (/-! ... -/).

3. Converts @[blueprint ...] attributes to declaration docstrings with a PROVIDED SOLUTION template, so that Aristotle can read the informal proof strategy as context:

/-- **CH2 Proposition 2.3, substep 1**

Let $a_n$ be a sequence with ...

PROVIDED SOLUTION:
Use Lemma first-fourier and Lemma second-fourier, similar to the proof of `limiting_fourier_aux`.
-/
theorem prop_2_3_1 ... := by
  sorry

4. Replaces completed proofs with admit so that Aristotle ignores them entirely and focuses its resources on the remaining sorrys.

5. Preserves sorry proofs as-is, which are the targets for Aristotle.

After conversion, a typical file will have some sorrys (the targets) surrounded by many admits (the already proven results).

2. Submit

To minimise the amount of time I have to wait for Aristotle to prove a theorem, I submit the file to the Aristotle API in parallel, one sorry at a time running the following submission script which automates this process:

scripts/aristotle_parallel_public.py PrimeNumberTheoremAnd/CH2Aristotle.lean --key YOUR_API_KEY

For each sorry in the file, the script:

1. Creates a temporary copy where that specific sorry is preserved and all other sorrys are replaced with admit.
2. Submits the copy to the Aristotle API as an independent job.
3. Polls until the job moves past NOT_STARTED before submitting the next one.

This means a file with 12 sorrys will result in 12 parallel Aristotle API requests, each focused on proving exactly one theorem.

You can also target specific sorrys:

# Submit only the first 5
scripts/aristotle_parallel_public.py file.lean -l 5

# Submit sorries 3 through 7 (1-indexed)
scripts/aristotle_parallel_public.py file.lean -r 3-7

# Submit from sorry 10 to the end
scripts/aristotle_parallel_public.py file.lean -r 10-

Requirements: pip install aristotlelib and an Aristotle API key (via --key flag or ARISTOTLE_API_KEY environment variable).

Call for Contributors

If you are interested in using Aristotle to contribute to PNT+ / IEANT, I would be happy to grant you write access to the pitmonticone/PNT fork.

If you are interested, please reply to this thread or send me a DM, and I will add you as a collaborator!

[Kim Morrison]

@Pietro Monticone, I surpised you don't mention any automation to poll for Aristotle results / validate them / incorporate them back into files.

[Pietro Monticone]

Yep, I know… I’ve been stupidly doing that part manually and pedantically reported the amount of manual effort in all PR bodies…

[Kim Morrison]

I've been wondering what an ideal Aristotle (/ general offline prover) interface looks like.

I like tactics, so my thought was:

• Replace a sorry with offline (backend := .aristotle) (or just the macro aristotle for that)
• It doesn't actually send anything off, it just does a sanity check that your local file is suitable for that backend and prints either an actionable error if not, or an info message (with "Try this:" suggestion) "This goal appears to be suitable for <BACKEND>. To send the request, please replace the tactic invocation with aristotle "a4cd66"", for some specified identifier that tactic has chosen in the background.
• This ensures that we only ever send off a "vetted" request, and don't spam the backend as we edit the file.
• That tactic now just displays a warning message, that will display a (cached, with X minute TTL) message about the progress at aristotle. You can edit the file, and it won't send off any new requests.
• Once the aristotle "a4cd66" tactic finds that the backend has finished, it changes to a info message with a Try this suggestion, which will attempt to just replace the current file with the Aristotle result (possibly post cleanup), if the file is still identical (or close enough?) to the state when the request was sent (possibly changing some admits in the request back to sorry, etc, possibly ignoring sorries filled in with proofs in the meantime, etc), and if it can't confidently paste in the results, instead it just tells you to the path of the result file, which presumably by now it has dropped in the same directory for you.