Discussion thread for Aristotle API

Stream: mathlib4

[Yury G. Kudryashov]

This is a discussion thread for #announce > Sign Up for the Aristotle API! .

[Alfredo Moreira-Rosa]

There was this discussion thread also started :
#Machine Learning for Theorem Proving > Sign Up for the Aristotle API!

[Yury G. Kudryashov]

It wasn't mentioned in the announcement thread, so I've started a new one. Also, the #Machine Learning for Theorem Proving channel is for people who're interested in developing/benchmarking/... AI systems, and I want the discussion to be visible to people who may want to use it without diving into AI development.

[Yury G. Kudryashov]

With my Harmonic hat on

We encourage you to try Aristotle on real-world sorrys in your draft contributions to Mathlib, your own projects, or just small experiments! We aim to make the system useful for people who work on formalizing any kind of mathematics, from school questions to research problems.
Please report any limitations of the system back to us.

With my Mathlib maintainer hat on

• If you plan to contribute Aristotle-generated code to Mathlib, then be prepared to clean it up before making your PR non-draft. Aristotle aims to close the goal by any means available, not to write a Mathlib-style code. E.g., it uses non-closing simps or even aesops a lot.
• You should read and understand the proofs. The reviewers will talk to you, not Aristotle, about this code.
• Aristotle is happy to exploit bugs in your formalizations. If it gives you a very short proof of a difficult problem, then possibly it found a contradiction in your assumptions instead of proving what you've meant to prove.
• Please add https://github.com/Aristotle-Harmonic as a co-author to your PRs, if it contributed a substantial amount of code.

[Floris van Doorn]

Does Harmonic store all queries made to the API? (I wouldn't mind if it did, but it's good to know.)

[Yury G. Kudryashov]

Yes.

[(deleted)]

Wow looks like the API is quite fast. When will there be a paid version of this API that is generally available

[(deleted)]

It beats GPT-5 hands down in terms of speed

[(deleted)]

And I imagine it will be much cheaper

[Yury G. Kudryashov]

We'll post here when it happens. I guess, I can't disclose any estimates before that because of the NDA.

[David Renshaw]

Aristotle is giving me proofs that seem to expect aesop to work as a non-terminal tactic. Is it using a custom version of aesop? Is there a way I can configure aesop locally to match it?

[David Renshaw]

Ah, I see this is just the default behavior of aesop, and Aristotle doesn't care about the warning

aesop: failed to prove the goal after exhaustive search.

[Yury G. Kudryashov]

Yes, we ignore the warning. When I fix style of a proof for Mathlib submission, I usually run aesop? on non-terminal aesops.

[Ryan Smith]

FYI I tried the sign up form twice and no email has ever come through

[(deleted)]

Yeah it's a wait-list after all

[(deleted)]

Some people are chosen some are not

[Yury G. Kudryashov]

Huỳnh Trần Khanh said:

Some people are chosen some are not

... yet. Please wait for a few more days.

[Chris Henson]

Are there plans to make the API available from a Lean tactic? (Or docs if I've overlooked it somehow)

[Eric Wieser]

Huỳnh Trần Khanh said:

Wow looks like the API is quite fast. When will there be a paid version of this API that is generally available

Huynh, assuming this means you have access: note that the terms of use of the API require you to "not develop, train, or improve any competing or substantially similar product or service", which seemingly applies in perpetuity, and even if you don't use the API to do so.

[Eric Wieser]

Which probably means contracted Lean data roles are incompatible with it (though of course I am not a lawyer)

[(deleted)]

I don't have access yet. I don't plan to use the API to create training data for machine learning but rather to do program verification. But yeah, looks like the wording is quite dangerous.

[Alfredo Moreira-Rosa]

Always amazed by these terms and conditions that can't be hold in court. Have they hired a proper lawyer?

[Ryan Smith]

Yury G. Kudryashov said:

Huỳnh Trần Khanh said:

Some people are chosen some are not

... yet. Please wait for a few more days.

No problem, I misunderstood it to mean general availability.

[Vikram Shanker]

ecyrbe said:

Always amazed by these terms and conditions that can't be hold in court. Have they hired a proper lawyer?

Hi @Eric Wieser and @ecyrbe ,

Thanks for the feedback on the terms. The goal is not to prevent people from the using the API, but rather to prevent folks from training on the outputs / using it to develop the same service. I'll share the feedback with our counsel and see if we can update the terms.

Best,
Vikram

[Kenny Lau]

we should have a formalised version of the T&Cs

[Eric Wieser]

Thanks Vikram; at the least I'd expect the item I quote to say something like "You should not use the API to develop, train, ...", rather than a blanket ban

[Jared green]

who actually has access by now though?(outside of Harmonic that is)

[Jared green]

and how is it at program verification

[Anthony Wang]

I just received my Aristole API key an hour ago and tried verifying an imperative program with mvcgen, but it didn't work because Aristole uses Lean v4.20.0-rc5 which predates mvcgen as well as grind. I haven't tried using it to verify functional programs yet.

[(deleted)]

Of course we can't expect any AI model to handle mvcgen

[(deleted)]

But that doesn't mean we can only prove properties of functional programs

[(deleted)]

You could roll your own monad and try

[Vikram Shanker]

we are working on more aggressively rolling out - anyone who has filled out the form should hear from me in the next 48 hours. As context, we've cleared about 1/3 of folks that signed up so far, and hope to get to 100% in the next week.

[Julian Berman]

Is there any preference for whether feedback is left here in this thread or replied via email?

[Vikram Shanker]

email is preferred, but we'll certainly be engaging here to the best of our ability :)

[Xinyi Zhang]

I'm developing a software which is a bit mix of differential cohomology and IMO abilities. Does this mean I can use the Aristotle?

[Lawrence Wu (llllvvuu)]

Yes, please try it and let us know your feedback!

[Jared green]

i looked at the instructions and i am confused. i have a file with a bunch of sorries waiting to be solved but the project it is in is set to v4.21. i take it i need to comment out any imports not coming from batteries or mathlib, but i would rather not make a new project just to do this. does the api solve entire files as though it was in a project with the prerequisites? also if it fails what goes into the output solutionfile?

[Yury G. Kudryashov]

It uploads all non mathlib dependencies of your file to the server, then stoves sorries in your file.

[Jakob von Raumer]

@Jared green If you're lucky none of your imports will conflict with v4.20. Just give it a try before you put in the work of making a new project. Be sure to call the api from the project directory for it to be able to resolve the imports.

[Jared green]

like, place the file that calls aristotle in the project, or have the present working directory be the project?

[Jared green]

also, the non mathlib imports have non-lean prerequisites but may not be essential to proving what is in the file.

[Alex Meiburg]

The working directory isn't relevant (afaict), the important thing is that your target file with sorries is inside of a lake project -- that is, if you go up in directories, you eventually find a file named "lakefile.lean", "lakefile.toml", or "lean-toolchain". Relevant imports are then pulled in using that a directory root. The following standard packages are already on the Harmonic server, at v4.20, and so won't be copied over:

    "Mathlib",
    "Lean",
    "Std",
    "Batteries",
    "Qq",
    "Aesop",
    "ProofWidgets",
    "ImportGraph",
    "LeanSearchClient",
    "Plausible",

Any other transitive imports /will/ be sent over. If something can't be found or can't be loaded, it will try its best to proceed anyway, but hard to say how much you'll get out.

[Alex Meiburg]

(This is all public information from the pip package source)

[Alex Meiburg]

You could comment out an import (in the target file, or any transitively imported files) that might make some of the declarations fail. As long as enough declarations are loaded that the sorries you care about can be loaded, you should be ok.

I mean, just in the generic sense that, in order to prove something, you need to an error-free declaration first. In general, errors in existing proof bodies can be handled mostly gracefully.

[Adrian Marti]

Anthony Wang said:

...Aristole uses Lean v4.20.0-rc5 which predates mvcgen as well as grind.

I don't think it predates grind though

[Yury G. Kudryashov]

grind was available but still experimental at that version.

[Jared green]

i tried to run provefromfile following the provided format and got an error:

python aristotlescript.py
File "C:\Users\jared\lean projects\aristotle_script\aristotlescript.py", line 7
solution = await aristotlelib.Project.prove_from_file("C:\Users\jared\lean projects\polysat2\Polysat2\Basic.lean")
^
SyntaxError: (unicode error) 'unicodeescape' codec can't decode bytes in position 2-3: truncated \UXXXXXXXX escape

[Eric Wieser]

You need r"C:\

[Jared green]

is there a way to terminate one of the proof searches? i ran the script over twelve hours ago, but found out on my own that one of the 'theorems' in my file probably has a counterexample, which i fixed and now i want to start it over again, but it is still waiting.

[Vikram Shanker]

Hi Jared,

For now there isn't a way to do this (we're working on it!), but feel free to update the file and just start a new search. You can run more than one in parallel!

[Jared green]

i dont want to overload the servers with abandoned searches using up compute resources that will come to nothing for me

[Asei Inoue]

can we use Aristotle by reap?

[Nick_adfor]

Vikram Shanker said:

we are working on more aggressively rolling out - anyone who has filled out the form should hear from me in the next 48 hours. As context, we've cleared about 1/3 of folks that signed up so far, and hope to get to 100% in the next week.

Well, till today I haven't received.

[Nick_adfor]

The time I registered is Oct.16

[Vikram Shanker]

@Nick_adfor it looks like you've gotten the key and are able to use the API now :)

[Vikram Shanker]

Hi Folks,

I'm happy to share that we have updated the terms of use and privacy policy to address feedback and concerns from the community. It should address concerns about the timeframe and scope of usage. Thanks for your patience while we updated them. Please feel free to let me know if there is additional feedback - our goal is make this a useful tool for the community to further research.

cc @Eric Wieser and @ecyrbe

[Aaron Hill]

aristotlelib has been reporting 'percent complete: 87' on each poll (as well as 'last updated at: 2025-10-24 00:46:03.333500') for several minutes. Is this expected?

[Vikram Shanker]

hi Aaron, I'll take a look at this shortly and follow up privately. For context, a handful folks just hit us with massive requests.

[Kim Morrison]

Could someone else with API access please test out #30842?

You should be able to use cmd-shift-p > Run Task > Aristotle: Prove Current File.

[Chris Henson]

Kim Morrison said:

Could someone else with API access please test out #30842?

You should be able to use cmd-shift-p > Run Task > Aristotle: Prove Current File.

This worked for me.

[Chris Henson]

Chris Henson said:

Are there plans to make the API available from a Lean tactic? (Or docs if I've overlooked it somehow)

I do still hope this is eventually possible, though I appreciate the potential difficulties.

[Nick_adfor]

(deleted)

[Nick_adfor]

(deleted)

[Nick_adfor]

(deleted)

[Eric Wieser]

Nick_adfor said:

Aristotle failed to find a proof.

The web editor says this statement has a type error

[Nick_adfor]

Eric Wieser said:

Nick_adfor said:

Aristotle failed to find a proof.

The web editor says this statement has a type error

Sorry. It should be

import Mathlib

open Matrix

variable {n : Type*} [Fintype n] [DecidableEq n]

theorem even_dim_of_A_sq_plus_id_eq_zero (A : Matrix n n ℝ) (h : A ^ 2 + (1 : Matrix n n ℝ) = 0) :
    ∃ m : ℕ, Fintype.card n = 2 * m := by admit -- already proved

theorem similar_to_block_form_simple (A : Matrix n n ℝ) (h : A ^ 2 + 1 = 0) :
    ∃ (m : ℕ) (hcard : Fintype.card n = 2 * m) (P : Matrix n n ℝ),
      IsUnit P ∧
      let e := Fintype.equivFinOfCardEq hcard
      let B : Matrix (Fin (2 * m)) (Fin (2 * m)) ℝ :=
        fun i j =>
          let i' : ℕ := i.val
          let j' : ℕ := j.val
          if i' < m ∧ j' = i' + m then -1 else
          if i' ≥ m ∧ j' = i' - m then 1 else 0
      P * A * P⁻¹ = reindex e.symm e.symm B := by
  sorry

[Nick_adfor]

(deleted)

[Janos Wolosz]

For Linux/macOS (or WSL) users with Aristotle API key: I've created a few shell scripts to simplify working with the Aristotle API. Feel free to try it out:
https://github.com/jano-wol/aristotle

[Kevin Buzzard]

Hi. Sorry for the basic question. I have some basic boilerplate lemma which I want to prove about module topologies and I thought that this would be a good test case for Aristotle; I've had an API key for ages but I've never used it. So I thought I'd try getting things up and running on my mac following https://pypi.org/project/aristotlelib/ and I've fallen at the first hurdle:

buzzard@IC-HWDXTW69VR FLT % pip3 install aristotlelib
Defaulting to user installation because normal site-packages is not writeable
ERROR: Ignored the following versions that require a different python version: 0.1.0 Requires-Python >=3.10; 0.1.1 Requires-Python >=3.10; 0.1.2 Requires-Python >=3.10; 0.2.0 Requires-Python >=3.10; 0.2.1 Requires-Python >=3.10; 0.2.2 Requires-Python >=3.10; 0.2.3 Requires-Python >=3.10; 0.2.4 Requires-Python >=3.10; 0.2.5 Requires-Python >=3.10; 0.3.0 Requires-Python >=3.10; 0.4.0 Requires-Python >=3.10; 0.4.1 Requires-Python >=3.10; 0.4.2 Requires-Python >=3.10; 0.4.3 Requires-Python >=3.10
ERROR: Could not find a version that satisfies the requirement aristotlelib (from versions: none)
ERROR: No matching distribution found for aristotlelib
buzzard@IC-HWDXTW69VR FLT %

My main problem is that I am only a recent mac user and I have no understanding of how the python ecosystem interacts with the mac ecosystem. Certainly python3 --version is returning Python 3.9.6. I asked Claude and Claude suggested I could (a) install Python 3.10 with brew (I have brew installed) (b) use pyenv or (c) use a virtual environment.

On my Ubuntu machine, where I understand what's going on a little better, I would say that (a) would be a catastrophic idea as changing the system version of python would presumably just break tons of stuff. I've never heard of pyenv so can't comment on (b). Regarding (c) I have used virtual environments before to run leanblueprint on my mac, but for some reason leanblueprint just worked out of the box after I factory reset it recently. What I am concerned about is that if I make a decision to follow one of these paths then using aristotle would somehow be inconvenient. Is there a recommended way to proceed here?

[Julian Berman]

You do not want to change your system python version, correct. My suggestion these days personally is brew install uv followed by uv run --with aristotlelib python foo.py

[Julian Berman]

(So, choice (d)).

[Julian Berman]

If you want to follow what Claude told you, brew install python3.13 is perfectly fine, but will not end up on your PATH by default. And you will still then want a virtual environment.

[Kevin Buzzard]

brew install uv
OK that bit worked
uv run --with aristotlelib python foo.py
But I don't have foo.py. I have my_file_with_a_sorry_in.lean. I'm sorry to be so dense. Which of the myriad files at https://pypi.org/project/aristotlelib/ is foo.py supposed to be? I count about 8 files which look like python files.

[Yury G. Kudryashov]

There's an executable aristotle in the package.

[Kevin Buzzard]

I am totally out of my depth. I do not even know which of the instructions on the aristotle website I am supposed to be following at this point. I have a lean file with a sorry in. I have installed uv. I have an API key. I have no understanding of python. What do I type next? I am genuinely sorry to be so clueless. I would ask an LLM but I trust the people here much more.

[Julian Berman]

Sorry Kevin -- I was assuming you were doing 4. Prove a theorem from a file from the README of aristotlelib -- if you're using the CLI, then my instruction is uvx --from aristotlelib aristotle prove-from-file my_file_with_a_sorry_in.lean

[Julian Berman]

(uvx is a thing that was installed alongside uv if you care to know)

[Kevin Buzzard]

Many thanks Julian! My impression is that it might be working now (I am seeing ongoing output saying things like status : IN_PROGRESS)

[Julian Berman]

Great. And now if you want to just be able to run aristotle without the first bit, you can run uv tool install aristotlelib. Or you go on with life as is.

[Kevin Buzzard]

I'm totally happy with the CLI solution for now! Many thanks!

[Kim Morrison]

@Kevin Buzzard I'm very surprised that you spent time on this, and yet are apparently opposed to efforts to make it easier, e.g. #PR reviews > aristotle task for command palette @ 💬 . :-)

[Kevin Buzzard]

Yeah, all I'm saying is that there is another point of view here, which is "if you want feature X then you figure out how to install it yourself" as opposed to "you will have feature X installed for you despite the fact that if you don't have an API key then it won't even work"

[Kevin Buzzard]

Maybe it's worth having some blog post or page on the community website saying "here are a ton of extra bells and whistles which you can add to your set-up together with instructions on how to do so"

[Kelly Davis]

Thanks for letting us try everything out early!

Kicking the tires a bit, it seems as if the newest version (aristotlelib 0.5.0) has a few bugs in relation to ingestion of informal theorems to be proven.

First, the project's PyPi page says informal theorems can be ingested as follows

aristotle prove-from-file path/to/problem.txt --informal

However, the help from the command line tool says something different

usage: aristotle prove-from-file [-h] [--api-key API_KEY] [--silent] [--output-file OUTPUT_FILE] [--no-auto-add-imports] [--context-files [CONTEXT_FILES ...]] [--no-validate-lean-project] [--no-wait] [--polling-interval POLLING_INTERVAL] [--max-polling-failures MAX_POLLING_FAILURES] [--informal] input_file

Note the input file is the final argument according to help.

Trying it with a simple example

(.venv) kdavis@Kellys-MacBook-Pro aristotlelib % cat informal-test.txt
Prove that the sum of two even numbers is even

one finds using the PyPi ordering, i.e. informal-test.txt  second to last, gives

(.venv) kdavis@Kellys-MacBook-Pro aristotlelib % aristotle prove-from-file informal-test.txt --informal
INFO - Validating input...
INFO - Found outermost project root at /Users/kdavis/Code/Aristotle/aristotlelib
Traceback (most recent call last):
  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/bin/aristotle", line 7, in <module>
    sys.exit(main())
             ~~~~^^
  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/cli/controller.py", line 42, in main
    return args.func(args)
           ~~~~~~~~~^^^^^^
  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/cli/api_action.py", line 82, in run
    asyncio.run(self.run_action(args))
    ~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/homebrew/Cellar/python@3.13/3.13.5/Frameworks/Python.framework/Versions/3.13/lib/python3.13/asyncio/runners.py", line 195, in run
    return runner.run(main)
           ~~~~~~~~~~^^^^^^
  File "/opt/homebrew/Cellar/python@3.13/3.13.5/Frameworks/Python.framework/Versions/3.13/lib/python3.13/asyncio/runners.py", line 118, in run
    return self._loop.run_until_complete(task)
           ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^^^^^^
  File "/opt/homebrew/Cellar/python@3.13/3.13.5/Frameworks/Python.framework/Versions/3.13/lib/python3.13/asyncio/base_events.py", line 725, in run_until_complete
    return future.result()
           ~~~~~~~~~~~~~^^
  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/cli/prove_from_file.py", line 91, in run_action
    await Project.prove_from_file(input_file_path=args.input_file, **kwargs)
  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/project.py", line 373, in prove_from_file
    local_file_utils.validate_local_file_path(
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^
        input_file_path, project_root=project_root
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    )
    ^
  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/local_file_utils.py", line 113, in validate_local_file_path
    raise ValueError(f"File {resolved_path} is not a Lean file")
ValueError: File /Users/kdavis/Code/Aristotle/aristotlelib/informal-test.txt is not a Lean file

using the help file ordering, i.e. informal-test.txt  last:

(.venv) kdavis@Kellys-MacBook-Pro aristotlelib % aristotle prove-from-file --informal informal-test.txt

INFO - Validating input...

INFO - Found outermost project root at /Users/kdavis/Code/Aristotle/aristotlelib

Traceback (most recent call last):

  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/bin/aristotle", line 7, in <module>

    sys.exit(main**()**)

             ~~~~**^^**

  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/cli/controller.py", line 42, in main

    return args.func**(args)**

           ~~~~~~~~~**^^^^^^**

  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/cli/api_action.py", line 82, in run

    asyncio.run**(self.run_action(args))**

    ~~~~~~~~~~~**^^^^^^^^^^^^^^^^^^^^^^^**

  File "/opt/homebrew/Cellar/python@3.13/3.13.5/Frameworks/Python.framework/Versions/3.13/lib/python3.13/asyncio/runners.py", line 195, in run

    return runner.run**(main)**

           ~~~~~~~~~~**^^^^^^**

  File "/opt/homebrew/Cellar/python@3.13/3.13.5/Frameworks/Python.framework/Versions/3.13/lib/python3.13/asyncio/runners.py", line 118, in run

    return self._loop.run_until_complete**(task)**

           ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~**^^^^^^**

  File "/opt/homebrew/Cellar/python@3.13/3.13.5/Frameworks/Python.framework/Versions/3.13/lib/python3.13/asyncio/base_events.py", line 725, in run_until_complete

    return future.result**()**

           ~~~~~~~~~~~~~**^^**

  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/cli/prove_from_file.py", line 91, in run_action

    await Project.prove_from_file(input_file_path=args.input_file, **kwargs)

  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/project.py", line 373, in prove_from_file

    local_file_utils.validate_local_file_path**(**

    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~**^**

        **input_file_path, project_root=project_root**

        **^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^**

    **)**

    **^**

  File "/Users/kdavis/Code/Aristotle/aristotlelib/.venv/lib/python3.13/site-packages/aristotlelib/local_file_utils.py", line 113, in validate_local_file_path

    raise ValueError(f"File {resolved_path} is not a Lean file")
**ValueError**: File /Users/kdavis/Code/Aristotle/aristotlelib/informal-test.txt is not a Lean file

Basically both suggested means of ingestion fail.

PS: I suggest using typer and rich for a much more modern, buttoned-down CLI experience. I've used them to good effect on goedels-poetry which does much of what Aristotle does.

[Kelly Davis]

PPS: Yury, just to make sure you get notified a ping @Yury G. Kudryashov

[Eric Rodriguez]

Thank you Kelly! Will make sure the team sorts this

[Kelly Davis]

In case anyone else sees this...

The work-around I found is to name your files <something>.lean, then both command line orderings work. The .lean suffix, even for informal theorems, seems to be required.

[Filippo A. E. Nuccio]

I' ve tried running Aristotle on a small file where I inserted a tex statement. It failed, but when I converted to a .lean file (just changing the extension) it was happier, although it of course immediately failed since the tex file was not written in lean syntax. Where can I find a reasonable doc for the autoformalization feature (eg: how should the file be saved, must it compile as stand-alone tex file, what command should I use, etc..)?

[Kelly Davis]

I've had success with just plain text...

(.venv) kdavis@Kellys-MacBook-Pro aristotlelib % cat informal-test.lean
Prove that the sum of two even numbers is even

executed, say, as

aristotle prove-from-file --informal informal-test.lean

[Kelly Davis]

Maybe you were missing the --informal argument?

To find more info use the --help argument

(.venv) kdavis@Kellys-MacBook-Pro aristotlelib % aristotle prove-from-file --help

usage: aristotle prove-from-file [-h] [--api-key API_KEY] [--silent] [--output-file OUTPUT_FILE] [--no-auto-add-imports] [--context-files [CONTEXT_FILES ...]] [--no-validate-lean-project] [--no-wait] [--polling-interval POLLING_INTERVAL] [--max-polling-failures MAX_POLLING_FAILURES] [--informal] input_file

Prove theorems from a Lean file

positional arguments:

  input_file            Path to the Lean file to prove

options:

  -h, --help            show this help message and exit

  --api-key API_KEY     Aristotle API key (can also be set via ARISTOTLE_API_KEY environment variable)

  --silent              Don't print any output to the console

  --output-file OUTPUT_FILE

                        Path to save the solution file (default: [input-file-name]_aristotle.lean)

  --no-auto-add-imports

                        Disable automatic import resolution (default: enabled)

  --context-files [CONTEXT_FILES ...]

                        Additional context files to include (cannot be used with auto-add-imports)

  --no-validate-lean-project

                        Skip Lean project validation (default: validate)

  --no-wait             Don't wait for completion; just kick it off (default: wait)

  --polling-interval POLLING_INTERVAL

                        Polling interval in seconds when waiting for completion (default: 30)

  --max-polling-failures MAX_POLLING_FAILURES

                        Max polling failures before exiting early. Proof might still be working in the background. (default: 3)

  --informal            Use informal input mode instead of formal Lean (default: formal Lean)

[Filippo A. E. Nuccio]

Yes, thanks!

[Vikram Shanker]

Hi Kelly,

Apologies for the bug here. Thanks for your detailed feedback and diagnosis. This is high on the list to fix / improve. I expect to have a fix shipped by Monday, if not earlier over the weekend.

Best,
Vikram

[Vikram Shanker]

@

Filippo A. E. Nuccio said:

I' ve tried running Aristotle on a small file where I inserted a tex statement. It failed, but when I converted to a .lean file (just changing the extension) it was happier, although it of course immediately failed since the tex file was not written in lean syntax. Where can I find a reasonable doc for the autoformalization feature (eg: how should the file be saved, must it compile as stand-alone tex file, what command should I use, etc..)?

Hi Filippo,

We're going to work on supporting a mixed more clearly in the coming days, I'll follow up with you when that is out.

Best,
Vikram

[Filippo A. E. Nuccio]

Sure, thanks @Vikram Shanker !

[Ryan Smith]

Did it end up proving your lemmas for you? I've only tried out aristotle a little bit so far, it's been a little hit or miss so far. Some things which can be done in just a couple lines baffle it, but it has closed some rather involved sorries as well.

[Nick_adfor]

I may ask for help, as Aristotle seems to find a counterexample for me, but Lean cannot run the "conterexample"

import Mathlib

open Lean Meta Elab Tactic in
elab "revert_all" : tactic => do
  let goals ← getGoals
  let mut newGoals : List MVarId := []
  for mvarId in goals do
    newGoals := newGoals.append [(← mvarId.revertAll)]
  setGoals newGoals

open Lean.Elab.Tactic in
macro "negate_state" : tactic => `(tactic|
  (
    guard_goal_nums 1
    revert_all
    refine @(((by admit) : ∀ {p : Prop}, ¬p → p) ?_)
    try push_neg
  )
)

open MvPolynomial

lemma coeff_Q_ne_zero {m : ℕ} (h : MvPolynomial (Fin (k + 1)) (ZMod p))
    (c : Fin (k + 1) → ℕ) (E : Multiset (ZMod p)) (hE_card : E.card = m)
    (sumX : MvPolynomial (Fin (k + 1)) (ZMod p))
    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) (sumX ^ m * h) ≠ 0) :
    MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)
    (h * (E.map (fun e => sumX - C e)).prod) ≠ 0 := by
  intro H
  apply h_coeff
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- Let's choose $p = 2$, $k = 1$, and $m = 1$.
  use 2, ⟨by norm_num⟩, 1, 1;
  -- Let's choose $h = x_0$.
  use MvPolynomial.X 0;
  -- Let's choose $c = (1, 0)$.
  use ![1, 0];
  refine' ⟨ { 1 }, _, _ ⟩ <;> norm_num;
  refine' ⟨ 1, _, _, _ ⟩ <;> norm_num;
  · simp +decide [ MvPolynomial.coeff_X' ];
    ext i ; fin_cases i <;> simp +decide;
  · simp +decide [ MvPolynomial.coeff_X' ];
    ext i ; fin_cases i <;> simp +decide

[Nick_adfor]

So I may ask if it is really a counterexample?...?

[Filippo A. E. Nuccio]

No, it did not prove it (but it was probably a bit hard). I'm trying on other, easier, things, and will report to @Vikram Shanker (or here).

[Filippo A. E. Nuccio]

No, it did not prove it (but it was probably a bit hard). I'm trying on other, easier, things, and will report to @Vikram Shanker (or here).

[Yury G. Kudryashov]

@Nick_adfor Here is a counterexample that works. I guess, our system has a bug with handling of autoimplicits (or the posted version of negate_state is not exactly what we use). We're investigating it.

import Mathlib

open Lean Meta Elab Tactic in
elab "revert_all" : tactic => do
  let goals ← getGoals
  let mut newGoals : List MVarId := []
  for mvarId in goals do
    newGoals := newGoals.append [(← mvarId.revertAll)]
  setGoals newGoals

open Lean.Elab.Tactic in
macro "negate_state" : tactic => `(tactic|
  (
    guard_goal_nums 1
    revert_all
    refine @(((by admit) : ∀ {p : Prop}, ¬p → p) ?_)
    try push_neg
  )
)

open MvPolynomial

lemma coeff_Q_ne_zero {m : ℕ} (h : MvPolynomial (Fin (k + 1)) (ZMod p))
    (c : Fin (k + 1) → ℕ) (E : Multiset (ZMod p)) (hE_card : E.card = m)
    (sumX : MvPolynomial (Fin (k + 1)) (ZMod p))
    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) (sumX ^ m * h) ≠ 0) :
    MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)
    (h * (E.map (fun e => sumX - C e)).prod) ≠ 0 := by
  intro H
  apply h_coeff
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- Let's choose $p = 2$, $k = 1$, and $m = 1$.
  use 1, 2, 1;
  -- Let's choose $h = x_0$.
  use MvPolynomial.X 0;
  -- Let's choose $c = (1, 0)$.
  use ![1, 0];
  refine' ⟨ { 1 }, _, _ ⟩ <;> norm_num;
  refine' ⟨ 1, _, _, _ ⟩ <;> norm_num;
  · simp +decide [ MvPolynomial.coeff_X' ];
    ext i ; fin_cases i <;> simp +decide;
  · simp +decide [ MvPolynomial.coeff_X' ];
    ext i ; fin_cases i <;> simp +decide

[Yury G. Kudryashov]

The only change is on the first use line.

[Nick_adfor]

Okay, now I understand this as a counterexample.

[Yury G. Kudryashov]

In your original request, you had a variable {p : Nat} [Fact p.Prime] line. With this line, the counterexample works as is.

[Asei Inoue]

Aristotle provide premise selector?

[Yury G. Kudryashov]

Do you mean a premise selector for grind? Currently, no (at least, in the public interface). Aristotle acts like a black box that produces proofs of sorrys, possibly adding extra lemmas. Or as a black box autoformalizing problems in natural language.

[Nick_adfor]

I receive an interesting email from Aristotle. Seems that after I close my vscode, Aristotle still works online. But not work out.

Hi,

Aristotle has finished working on your project, and the results are now ready for you to review!

You can find your verified solution attached to this email, and also via the Aristotle Terminal Interface.

Happy proving!
The Aristotle Team

If you would like to stop receiving email notifications from Aristotle, please reply to this email and we will disable them within 48 hours.

/-
This file was edited by Aristotle.

Lean Toolchain version: leanprover/lean4:v4.20.0-rc5
Mathlib version: d62eab0cc36ea522904895389c301cf8d844fd69 (May 9, 2025)
-/

import Mathlib


variable {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ}

open MvPolynomial

/- Aristotle failed to find a proof. -/
lemma coeff_Q_ne_zero {m : ℕ} (h : MvPolynomial (Fin (k + 1)) (ZMod p))
    (c : Fin (k + 1) → ℕ) (E : Multiset (ZMod p)) (hE_card : E.card = m)
    (sumX : MvPolynomial (Fin (k + 1)) (ZMod p))
    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) (sumX ^ m * h) ≠ 0) :
    MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)
    (h * (E.map (fun e => sumX - C e)).prod) ≠ 0 := by
  sorry

/- Aristotle failed to find a proof. -/
lemma Q_total_degree_eq_sum_c (h : MvPolynomial (Fin (k + 1)) (ZMod p))
    (A : Fin (k + 1) → Finset (ZMod p))
    (c : Fin (k + 1) → ℕ)
    (hA : ∀ i, (A i).card = c i + 1)
    (m : ℕ) (hm : m = (∑ i, c i) - h.totalDegree)
    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)
              ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * h) ≠ 0)
    (E : Multiset (ZMod p)) (hE_card : E.card = m)
    (sumX : MvPolynomial (Fin (k + 1)) (ZMod p))
    (Q : MvPolynomial (Fin (k + 1)) (ZMod p))
    (hsumX_def : sumX = ∑ i, MvPolynomial.X i)
    (hQ_def : Q = h * (E.map (fun e => sumX - C e)).prod) :
    Q.totalDegree = ∑ i, c i := by
  sorry

[Nick_adfor]

In that case, may I ask if I can run the Python code to import the .lean file into Aristotle and then shut down my computer, since the process will be handled online and doesn’t need to run locally?

[Jakob von Raumer]

Yes, after submitting your project, everything is handled online and you can check back any time later.

[Nick_adfor]

Jakob von Raumer said:

Yes, after submitting your project, everything is handled online and you can check back any time later.

The most absurd thing just happened: I turned on my computer, heard its sound for nights, and then realized I Could have just closed it and waited for it to email me ???....???

[Nick_adfor]

Now I know why Aristotle ask me for email when register.

[Kim Morrison]

@Yury G. Kudryashov / @Vikram Shanker, some Aristotle wishlists:

• Aristotle doesn't put ; at the end of so many lines.
• and doesn't put spaces like rw [ X, Y ]
• doesn't use latex dollar signs to enclose Lean code in comments, and instead uses backticks
• omit types for arguments in lambdas more often
• use dot notation more often
• line wrap comments automatically

These would save time cleaning up proofs!

[Nick_adfor]

terrible things: 18h passed and Aristotle hasn't given me an email containing code.

[Matteo Del Vecchio]

@Nick_adfor In the new UI (see #announce > Launched: Aristotle Autoformalization Mode @ 💬 ) you can select "View History", then "Show all projects", then select the one you want and it should download the answer

[Vikram Shanker]

Kim Morrison said:

Yury G. Kudryashov / Vikram Shanker, some Aristotle wishlists:

• Aristotle doesn't put ; at the end of so many lines.
• and doesn't put spaces like rw [ X, Y ]
• doesn't use latex dollar signs to enclose Lean code in comments, and instead uses backticks
• omit types for arguments in lambdas more often
• use dot notation more often
• line wrap comments automatically

These would save time cleaning up proofs!

Thanks for the feedback Kim (and everyone else)!

[Siddhartha Gadgil]

@Vikram Shanker @Yury G. Kudryashov Just adding to the feedback based on recent (positive) experience.

• There are various exact? statements in the generated code. Making a meta-programming pass to replace these with the suggestions of TryThis would be nice.
• There are also a lot of non-terminal aesop statements that do make changes. I fear this makes the code fragile. I tried aesop? and replacing in these cases, but the result was not a valid proof.

[Siddhartha Gadgil]

A little update - the result is not as good as I hoped. This was an almost successful multi-AI story but not quite.

• My goal in the longer run is to be able to use numerical estimates to prove existence of zeroes, and hence many things like knottedness (by constructing SU(2) representations). @Dattabhasvant Ghadiyaram is working towards this and more.
• By general knowledge of Multivariable Calculus/Differential Topology, I was fairly sure that a result saying that if $f(x_0)$ is very close to $0$ and "effectively transversal" - the derivative is surjective with right inverse having bounded norm and the second derivative is bounded, we have a zero.
• Not surprisingly, ChatGPT could tell me that this is a special case of the "Newton-Kantorovich theorem".
• I asked ChatGPT to prove it in the special case that I wanted - functions between Euclidean spaces. I duly got a proof, which ChatGPT wrote up as a LaTeX file.
• I tested Aristotle's new autoformalization mode with this. After a day and a half I got a proof.
• The proof compiled successfully and the theorem was in some ways more general.
• Since the statement was complicated, I passed this back to ChatGPT to ask if this included the result I wanted.
• As pointed out by ChatGPT (and checked by me) unfortunately it did not. There was an extra hypothesis - the existence of a left inverse. This means the result only applied for equal dimensional spaces - a serious restriction.

Aristotle was impressive but not quite good enough here. This is also an example of how we need to check final statements after autoformalization, and LLMs can do this to some extent.

I also wonder to what extent Aristotle is digesting the source - the theorem proved was both more and less general than the source.

[Yury G. Kudryashov]

You can try replacing the main goal in the lean file you've got from Aristotle and sending it back to the API.

[Siddhartha Gadgil]

@Yury G. Kudryashov What do you mean "send it back"? Do you mean I change the goal, replace the proof by sorry and then ask for filling sorries?

[Yury G. Kudryashov]

Yes, or add a new version of the theorem with := by sorry after the existing lemmas & the old "main" theorem.

[Siddhartha Gadgil]

Thanks. Launched that

[Alex J. Best]

Hi @Siddhartha Gadgil thanks for trying Aristotle, we appreciate your feedback and will work on it!
However regarding your experience with Newton-Kantorovich, we took a look and think this is actually an excellent demonstration of the power of formalization and benefit of Aristotle over ChatGPT and friends.
In the informal proof you submitted ChatGPT itself confuses left inverses and right inverses, and the proof it gives is actually only valid in the equidimensional case without additional work. Aristotle noted this "implicit assumption" (aka mistake) in GPT's proof and correctly added it to the formal version. This is really the power of formalization when working with LLMs.
We'll try to ensure that the output makes situations like this clearer, and the agent explains why adding assumptions was necessary in such cases.

For completeness for anyone following along, Aristotle put

(h_left_inv : T ∘L fderiv ℝ f x₀ = ContinuousLinearMap.id ℝ E) :

because GPT put the following statement

"Since $T$ is a right inverse of $DF(x_0)$, T DF(x_0) = 1"

in the informal proof.

[Siddhartha Gadgil]

@Alex J. Best I see, thanks. Ideally there should be back-and-forth and ChatGPT's result should be fixed. Mathematically what is needed is only an effective surjection.

[Siddhartha Gadgil]

@Alex J. Best A comment about what Aristotle tried to prove. The statement included that the Newton iteration converges to the given point. This is really a detail one wants to abstract away from the statement - all one wants is the existence of the zero (uniqueness was also added, but this can be considered a bonus).

[Junyan Xu]

I upgraded to aristotlelib 0.5.0 today and used it the first time to solve some sorries. It's wonderful that Aristotle came back with the solution in ~20 minutes! Two issues I encountered:

1. after upgrading to 0.5.0, running aristotle in cmd (on Windows) didn't immediately work; I spent several round of conversations with Claude to figure out that aristotle.exe is located in C:\Users\xujys\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.12_qbz5n2kfra8p0\LocalCache\local-packages\Python312\Scripts in my case. Could the path be automatically added to the PATH environment variable?

2. Some decls in my code changed names since May, so Aristotle encountered an error, and I had to clone another copy of mathlib and spin up d62eab0cc36ea522904895389c301cf8d844fd69 to fix the error. Would you consider hosting a web editor on that commit of mathlib?
   (Looks like some .olean.server files (from the new module system?) were not cleaned away by lake exe cache get and Lean reports "incompatible header" error on them, and lake clean was taking too long, so I couldn't use an existing clone of mathlib.)

Thanks for granting me access to your great AI system and your hard work! When it comes to making a PR, it seems the convention for acknowledgement is Co-authored-by: Aristotle Harmonic <aristotle-harmonic@harmonic.fun> in the PR description and authorship (but not copyright) in the file header (example); did I get it right?

[Siddhartha Gadgil]

Junyan Xu said:

I upgraded to aristotlelib 0.5.0 today and used it the first time to solve some sorries. It's wonderful that Aristotle came back with the solution in ~20 minutes! Two issues I encountered:

1. after upgrading to 0.5.0, running aristotle in cmd (on Windows) didn't immediately work; I spent several round of conversations with Claude to figure out that aristotle.exe is located in C:\Users\xujys\AppData\Local\Packages\PythonSoftwareFoundation.Python.3.12_qbz5n2kfra8p0\LocalCache\local-packages\Python312\Scripts in my case. Could the path be automatically added to the PATH environment variable?

2. Some decls in my code changed names since May, so Aristotle encountered an error, and I had to clone another copy of mathlib and spin up d62eab0cc36ea522904895389c301cf8d844fd69 to fix the error. Would you consider hosting a web editor on that commit of mathlib?
   (Looks like some .olean.server files (from the new module system?) were not cleaned away by lake exe cache get and Lean reports "incompatible header" error on them, and lake clean was taking too long, so I couldn't use an existing clone of mathlib.)

Thanks for granting me access to your great AI system and your hard work! When it comes to making a PR, it seems the convention for acknowledgement is Co-authored-by: Aristotle Harmonic <aristotle-harmonic@harmonic.fun> in the PR description and authorship (but not copyright) in the file header (example); did I get it right?

I also would very much like a hosted server corresponding to Aristotle's toolchain

[Eric Wieser]

Junyan Xu said:

Could the path be automatically added to the PATH environment variable?

This is a question that python asks you when you install it for the first time

[Junyan Xu]

• There are also a lot of non-terminal aesop statements that do make changes. I fear this makes the code fragile. I tried aesop? and replacing in these cases, but the result was not a valid proof.

Let me note that in my example, each time aesop is used in Aristotle's code it fails to close the goal and acts effectively as intros; the only difference is that intros assigns inaccessible names to the variables while aesop assigns the original names. Maybe Aristotle has learned to use aesop to introduce nicely named variables ...

[Yury G. Kudryashov]

Aristotle has learned to use aesop for "general cleanup" of the goal state, that includes intro, constructor, cases etc.

[Junyan Xu]

This is a question that python asks you when you install it for the first time

I can run python and pip without specifying the path though; somehow the installer fails to add the Scripts folder to PATH? Anyway it would be nice to inform the user in the aristotlelib instructions.

[Yury G. Kudryashov]

It may be a windows-specific issue. Usually, I'm creating a python virtual environment and install whatever I need into that environment.

[Gavin Zhao]

From reading the thread, it seems like it is expected that Aristotle takes ~20 minutes to process even short simple theorems?

[Gavin Zhao]

So Aristotle is more suitable for long or complex proofs?

[Yury G. Kudryashov]

We have a queue of requests. We may increase the bandwidth for the public API later.

[Yury G. Kudryashov]

You can use it for simple proofs, if you just leave them as sorry on your side and go on.

[Yury G. Kudryashov]

Then you copy+paste the proofs back to your file when they're ready.

[Gavin Zhao]

Sorry I should've clarified. The context is that I want to evaluate Aristotle's performance on (a slightly modified) FormalMATH benchmark. From my experience using aristotlelib programmatically, it takes ~20 minutes to output a single proof, this approach doesn't really scale.

[Yury G. Kudryashov]

Another way to use it is to write a skeleton file with many theorems you want to prove, then submit all of them.

[Gavin Zhao]

Oh so sort of batching requests in one file, interesting.

[Yury G. Kudryashov]

Gavin Zhao said:

Sorry I should've clarified. The context is that I want to evaluate Aristotle's performance on (a slightly modified) FormalMATH benchmark. From my experience using aristotlelib programmatically, it takes ~20 minutes to output a single proof, this approach doesn't really scale.

If you want to run a benchmark, then it may be better to contact @Vikram Shanker.

[Gavin Zhao]

Yury G. Kudryashov said:

Another way to use it is to write a skeleton file with many theorems you want to prove, then submit all of them.

I'm curious if the theorems are completely unrelated, does it causes quality degradation due to context "poisoning"?

[Gavin Zhao]

I've experienced this a lot with coding agents in general, but depending on the architecture of Aristotle the effects might be much smaller.

[Tudor]

Gavin Zhao said:

Yury G. Kudryashov said:

Another way to use it is to write a skeleton file with many theorems you want to prove, then submit all of them.

I'm curious if the theorems are completely unrelated, does it causes quality degradation due to context "poisoning"?

No, that hasn't really been an issue

[Gavin Zhao]

I see, thanks for the info!

[Vikram Shanker]

Hi @Kelly Davis thanks for your detailed feedback earlier. I pushed an update to the package which fixes the bug you reported (thanks again for such a great bug report). I also wanted to note that the TUI that you get when you just type aristole (no params) may be a better UX with a bit more info. Hope you check it out!

[Kim Morrison]

Siddhartha Gadgil said:

I also would very much like a hosted server corresponding to Aristotle's toolchain

Joachim made this happen! https://live.lean-lang.org/ now has Mathlib @ v4.20.0-rc5 (the version Aristotle is using right now) as well as Mathlib @ v4.24.0.

[Joachim Breitner]

Playing with aristotle for the first time, using the aristotle CLI tool and passing a natural language task, and now I am impatient :-)
Is

  │Status: IN_PROGRESS     [██████              ] 30%  |  Updated 25 secs ago                                                                                                                │

all I get to see while its running, or is there a way to see the output as it is progressing?

[Nick_adfor]

Let me joke that: maybe the percentage is a fake one as it will stuck at 99.99%

[Siddhartha Gadgil]

In my case the percentage was not even monotonic.

[Nick_adfor]

Not even monotonic ha:)

[Alex Meiburg]

Joachim Breitner said:

Is ... all I get to see while its running, or is there a way to see the output as it is progressing?

There's no way to see intermediate output at the moment, sorry. The percentage is a best guess. :)

[Chen Ling]

Should Aristotle AI provide an option to discard tasks? Recently, I tried it to fill sorries for me, but I forgot to attach the informal reference answer. Hours passed, It's still in progress.
When the task gets stuck, users will realize they need write more detailed informal answer, or break down a single sorry from the big theorem into several lemmas, then try again. It will also help save tokens :)

[TongKe Xue]

Is Aristotle currently meant for

1. async batch use only (i.e. write a file with lots of sorrys, submit it, look at it 20 minutes later)
2. or also for interactive use? i.e. I'm doing theorem proving. Whenever, my goal state changes, I want it to (1) kill my previous aristotle request, (2) submit current goal state as my aristotle request. Then, at any time, if aristotle finishes the rest of the proof before me, it notifies me and fills in the proof.
   (I realize this breaks the queue model, and may require 1 pre-emptive CPU per active user.)

[Gavin Zhao]

I would also really love to use Aristotle interactively!

[Nick_adfor]

I've found this: https://borisalexeev.com/t/Erdos367.lean

[Nick_adfor]

How does Aristotle solve it? I may think that Aristotle can only fill sorry. Can it generate new def and new lemma?

[Kevin Buzzard]

You're out of date -- that's last week's news. Today everyone's talking about https://www.erdosproblems.com/forum/thread/124

[Boris Alexeev]

Nick_adfor said:

How does Aristotle solve it? I may think that Aristotle can only fill sorry. Can it generate new def and new lemma?

Yes, Aristotle has an "informal" mode that accepts natural-language input (whether in LaTeX or just text). It also decomposes into smaller lemmas where necessary. These features were released "publicly" around November 20.

[Nick_adfor]

Boris Alexeev said:

Nick_adfor said:

How does Aristotle solve it? I may think that Aristotle can only fill sorry. Can it generate new def and new lemma?

Yes, Aristotle has an "informal" mode that accepts natural-language input (whether in LaTeX or just text). It also decomposes into smaller lemmas where necessary. These features were released "publicly" around November 20.

It's really a sad thing that since Aristotle failed to formalize the proof of Alon-Nathanson-Ruzsa Theorem (I've already write the lean statement, I want Aristotle to have a lean proof.), I've stopped using Aristotle for days : (

[Siddhartha Gadgil]

Continuing my updates, I got a run to the end without additional hypothesis (though after 2-3 crashes and 1 output with only the imports). The result is at https://github.com/siddhartha-gadgil/LeanAide/blob/main/Kantorovich-aristotle.lean

This is a little disappointing still as the theorem only states that the Newton-iteration converges, not that there is a 0. I will add this as a goal with "by sorry" and see if this completes the proof.

[Aaron Hill]

Siddhartha Gadgil said:

• There are various exact? statements in the generated code. Making a meta-programming pass to replace these with the suggestions of TryThis would be nice.

I also encountered this yesterday - there were several generated exact? statements, though all of them had a single (correct suggestion). After manually clicking 'apply' on all of them, I ended up with a valid proof

[Aaron Hill]

actually, it looks like the proof was sorry-free (via #print axioms) even with theexact?. I guess exact? elaborates to suggested term

[Alex J. Best]

Indeed exact? elaborates to the term it suggests, proofs using it are termwise identical to when you click the suggestion generally speaking.

[Filippo A. E. Nuccio]

Two minor feedbacks concerning the Aristotle API:

• the ctrl+c command to close the window works if I'm in the VSCode terminal, but not if I do everything from the bash (in which case I need to force-close the window); just for the context, I prefer to work from the bash since both ctrl+T and ctrl+F are taken by my VSCode preferences, and I cannot access the commands of the API (I find the 1-2-3-4 choices in the first window way more efficient);
• the files produced lack any import; I make it do adding an import Mathlib at the beginning, but I think adding this automatically should be easy (and, in the future, even minimizing imports a bit would be useful).

[Filippo A. E. Nuccio]

Alex J. Best said:

Indeed exact? elaborates to the term it suggests, proofs using it are termwise identical to when you click the suggestion generally speaking.

And is there a reason why it does not convert it to the elaborated term? If it was intentional to mark that the way aristotle found it was through an exact? this could appear in a comment, no?

[Siddhartha Gadgil]

As Filippo said it would make sense to convert the exact? tactics. This will also reduce the noise.

One practical issue is that there are so many warnings because of namespace issues, variable name reuse and especially aristotle failing to prove goals that the noise drowns out the one warning that I really care about, which is a proof using sorry.

[Nick_adfor]

Now I've a question:

import Mathlib

open scoped Finset

variable {R : Type*} [CommRing R]
variable {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ}

open MvPolynomial

open Finsupp


lemma h_total_degree : ∀ (s : Multiset (MvPolynomial (Fin (k + 1)) (ZMod p))), (∀ p ∈ s, p.totalDegree = 1) → s.prod.totalDegree = s.card := by
        bound
        induction s using Multiset.induction <;> aesop
        -- Apply the lemma that the total degree of a product is the sum of the total degrees, given that both factors are non-zero.
        have h_total_degree_mul : ∀ (f g : MvPolynomial (Fin (k + 1)) (ZMod p)), f ≠ 0 → g ≠ 0 → (f * g).totalDegree = f.totalDegree + g.totalDegree := by
          exact fun f g a a_3 => totalDegree_mul_of_isDomain a a_3
        by_cases h : a_1 = 0 <;> by_cases h' : s.prod = 0 <;> simp_all +decide [add_comm]
        rw [eq_comm] at a_2
        simp_all only [Multiset.card_eq_zero, Multiset.notMem_zero, IsEmpty.forall_iff, implies_true]

[Nick_adfor]

How Aristotle works with bound and aesop? Even it can work, I cannot understand :(((

[Nick_adfor]

There's thing like aesop? but here it cannot work. Also there's nothing like bound?, then how can I know how it works?

[Nick_adfor]

This part raise the maxHeartbeats of my whole code.

[Nick_adfor]

It seems a problem in  <;> aesop, not Aristotle

[Chen Ling]

It can even correct my formalization, show me the right one and prove it, amazing.

I wrote something related to Schur number, it told me why my formalization is wrong, and proved the following claim (the whole proof is 450+ lines):

theorem schur_distinct_nat (k : ℕ) : ∃ N : ℕ,
  ∀ (C : ℕ → Fin k), ∃ (a b c : ℕ),
    [a, b, c].Nodup ∧
    1 ≤ a ∧ a ≤ N ∧ 1 ≤ b ∧ b ≤ N ∧ 1 ≤ c ∧ c ≤ N ∧
    C a = C b ∧ C b = C c ∧
    a + b = c := by

schur_number.lean

I had no idea about the proof, and even made mistakes in formalization, but the powerful AI corrected and proved it.

However, still, I have no idea about the proof now. The AI-generated proof is full of unterminated aesop, and tactics like grind, generalize_proofs. It still requires considerable efforts to read the AI-generated lean4 proof, maybe not easier than read a human-written informal proof. Anyway, it's my problem, not Aristotle's.

[Nick_adfor]

Aristotle helps solve a Theorem! (Though the running time should be optimized)

#general > Formalize paper about Restricted Sums

[Alex Meiburg]

Nick_adfor said:

Also there's nothing like bound?

I have a PR for this actually, I admit the PR was mostly motivated by my own wanting to have this to improve Aristotle's outputs: #27262 (I haven't had time to touch it in a while)

But at the moment you can just do

aesop? (rule_sets := [Bound, -default]) (config := Mathlib.Tactic.Bound.boundConfig)

which is exactly equivalent to calling bound, with aesop?'s proof script generation.

[Mattias Ehatamm]

Has anyone successfully gotten Aristotle to work with non-mathlib project imports? I tried a few different things but was unable to get it to see definitions contained in the other project that were imported.

[Vikram Shanker]

Hi Mattias, this should work, but its possible there is a bug. Can you either email me a repro or jump on a quick call to debug? We can share the findings back to the thread!

[Mattias Ehatamm]

It's been a moment since I tried this, I'll reproduce and send you the repo

[Ronan Lamy]

Mattias Ehatamm said:

Has anyone successfully gotten Aristotle to work with non-mathlib project imports? I tried a few different things but was unable to get it to see definitions contained in the other project that were imported.

It works in PhysLean, see here. PhysLean depends only on mathlib though, so idk if that answers your question.

[Wang Jingting]

@Vikram Shanker Hi Vikram, it seems that my previous API key has expired, how could I apply for a new one? Do I need to submit the application form again?

[Vikram Shanker]

the key doesn't expire, but the link I used to share it does :) Feel free to email me and I'll send you a new link if you didn't save the key locally

[Kim Morrison]

@Vikram Shanker, an Aristotle bug report, that when sending a markdown file along with --context, Aristotle often gives results with names duplicated with existing names in the contextual files. E.g. I have an informal document with many results that have multiple parts in the statement, and Aristotle is formalizing them as theorem part_i, theorem part_ii (very nice!). But then it does the same in the next file, requiring manual intervention.

[Vikram Shanker]

thanks for the bug report! will follow up in DM for details

[Kim Morrison]

I'm not quite ready to share, but I have a somewhat lovely pipeline where:

1. We drop in a textbook PDF
2. We split into individual pages
3. Claude writes a script that runs pdftotext and identifies candidate start/end positions of theorems/lemmas/etc
4. Claude is told to spot check the results, and compare against the individual page PDFs (which it can read way better than the embedded text layer), and iteratively improve the position extraction script as it finds missing or incorrect positions.
5. In a loop, Claude is then told to read the page PDFs and extract the statements/proofs to markdown. (This consumes a lot of API tokens, but not crazy. Equivalent to ~24 hours quota of Claude Max.)
6. We generate a stub .lean file for every item in the book. The first imports Mathlib, otherwise each imports the previous. (This is a step that could be improved, by already doing dependency analysis, blueprint style.)
7. One item at a time, we send an extracted markdown file to Aristotle, along with the --context of all the previous Lean files.
8. Claude then reads Aristotle's output, and decides whether this counts as "attention needed", "statement formalized", or "proof formalized". It copies both the extracted markdown (as a module doc) and Aristotle's proof into file, ready for providing as context for the next run. It also does some minor cleanup (e.g. renaming duplicate theorem part_i; it could also do stylistic cleanup like expanding exact? but I haven't bothered).

[Kim Morrison]

It's not super useful for me to have done this, as the pipeline is easy to reproduce and I'm sure Harmonic will/already have worked out how to scale up to book scale PDFs. But it was a fun experiment to see what can be achieved by combining tools available today.

[Kim Morrison]

I won't share the repository publicly right now, as I started with a copyrighted PDF (Gorenstein's "Finite Groups") and although the actual PDF and text layers never get committed to the repository, I have been committing Claude's extracted markdown, which would certainly be covered by copyright.

[Kim Morrison]

The Claude extraction pipeline has run on the whole book. It's not 100% perfect, but spot checks indicate it is 99%! I was very surprised how good this is. The Aristotle+Claude formalization pipeline is about half way through Chapter 1. It's succeeded on everything through to Theorem 2.13, but couldn't complete the proofs in Theorem 2.7. It's worth noting that this is very much only the standard preliminary material, and I haven't got to the point where Aristotle is actually working on the real book contents, so we may see a dramatic drop-off in success once moving to the next chapter.

[Kim Morrison]

Note that I have not read the book at all, and none of my prompting to prepare this involves specific knowledge of the contents! (Beyond choosing what I knew to be a nicely self-contained book, which starts at a level that overlaps with Mathlib content.)

[Kim Morrison]

It's very impressive that Aristotle successfully writes some auxiliary definitions, and sometimes (would be nice if this were more consistent) splits multipart theorem statements into separate declarations. It's also really nice that often Aristotle will simply tell you that a theorem already exists in Mathlib, and give #check statements as evidence.

[Kim Morrison]

A pity the proofs themselves are so ... merely true. :-)

[Vikram Shanker]

@Kim Morrison I think if you use --formal-input-context you'll be able to avoid the naming issues

[Lawrence Wu (llllvvuu)]

Aristotle will only use results that have been imported transitively. It will additionally be able to read, but not use, files passed in as non-formal context.

[Lawrence Wu (llllvvuu)]

if each file imports the previous file you’ll probably have approximately the import graph that you want

[Kevin Buzzard]

Is there an easy way of getting Aristotle to try filling in sorries in FLT in a file which starts

import FLT.DedekindDomain.FiniteAdeleRing.BaseChange
import FLT.Mathlib.NumberTheory.NumberField.Basic
import FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

?

[Vikram Shanker]

have you tried it/ did you run into errors? I haven't looked tested this specifically but we do automatically trace the imports so if you use the sorry filling mode (mode 1), it should work

[Lawrence Wu (llllvvuu)]

Imports are generally not an issue for us, though of course the amount of files increases the probability that some file won’t load on our version of mathlib. It’s fine if proofs don’t compile, we only need to load the declarations, but this is a high enough bar with the frequency typeclass changes / removals without deprecation, etc in mathlib, that while it’s not an ideal situation, right now the most reliable way to get sorry-filling to work is to have a branch that matches our version (currently mathlib f897ebcf72cd16f89ab4577d0c826cd14afaafc7). https://mathlib-changelog.org/v4 streamlines this a bit.

[Lawrence Wu (llllvvuu)]

Another rough edge right now is that Aristotle will not add new imports, e.g. if there's something in FLT.Foo.Bar that you need but you didn't (transitively) import it, then it won't go and import it for you (in fact, it won't even be aware that it exists).

We just uploaded some slides at ItaLean that goes over Aristotle features and rough edges: https://github.com/pitmonticone/ItaLean2025/blob/main/presentations/AristotleTutorial.pdf

[Kevin Buzzard]

Vikram Shanker said:

have you tried it/ did you run into errors?

/-
This file was edited by Aristotle.

Lean version: leanprover/lean4:v4.24.0
Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
This project request had uuid: 90c874df-c85d-43f6-becc-6c1a4a766641

Aristotle encountered an error while processing imports for this file.
Error:
unknown module prefix 'FLT'

No directory 'FLT' or file 'FLT.olean' in the search path entries:
/code/harmonic-lean/.lake/packages/batteries/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/Qq/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/aesop/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/proofwidgets/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/importGraph/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/plausible/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/MD4Lean/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/BibtexQuery/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/UnicodeBasic/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/Cli/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/mathlib/.lake/build/lib/lean
/code/harmonic-lean/.lake/packages/doc-gen4/.lake/build/lib/lean
/code/harmonic-lean/.lake/build/lib/lean
/root/.elan/toolchains/leanprover--lean4---v4.24.0/lib/lean
/root/.elan/toolchains/leanprover--lean4---v4.24.0/lib/lean

-/

This was running the command line aristotle within the FLT directory.

[Kevin Buzzard]

Unfortunately I bump FLT about once a week typically, and bumps often break things (not least because stuff from FLT gets upstreamed to mathlib). However I could attempt to minimise and get some version of the repo compiling on commit f897ebcf72cd16f89ab4577d0c826cd14afaafc7 -- I will certainly have a version which compiles on a commit close to this. Is it likely that f897ebcf72cd16f89ab4577d0c826cd14afaafc7 will be "the Harmonic mathlib" for the foreseeable future?

[Lawrence Wu (llllvvuu)]

That actually looks like a bug in our frontend. We'll look into it, cc @Vikram Shanker

[Wang Jingting]

(deleted)

[Wang Jingting]

Vikram Shanker said:

the key doesn't expire, but the link I used to share it does :) Feel free to email me and I'll send you a new link if you didn't save the key locally

Thanks, I noticed that there's something I did wrong when exporting environment variables, it works properly now.

[Kim Morrison]

I (via :bot:) wrote a cleanup_aristotle.py script, which cleans up a number of easily fixable defects in current Aristotle proofs. Sharing in the hope that it is useful / someone makes it better / it prompts anyone to write a really nice Lean refactoring tool. :-)

[Lawrence Wu (llllvvuu)]

Nice, thanks! Another one people often ask us for is attempting to replace native_decide with decide, or failing that, decide +kernel

[Nick_adfor]

Kim Morrison said:

I'm not quite ready to share, but I have a somewhat lovely pipeline where:

1. We drop in a textbook PDF
2. We split into individual pages
3. Claude writes a script that runs pdftotext and identifies candidate start/end positions of theorems/lemmas/etc
4. Claude is told to spot check the results, and compare against the individual page PDFs (which it can read way better than the embedded text layer), and iteratively improve the position extraction script as it finds missing or incorrect positions.
5. In a loop, Claude is then told to read the page PDFs and extract the statements/proofs to markdown. (This consumes a lot of API tokens, but not crazy. Equivalent to ~24 hours quota of Claude Max.)
6. We generate a stub .lean file for every item in the book. The first imports Mathlib, otherwise each imports the previous. (This is a step that could be improved, by already doing dependency analysis, blueprint style.)
7. One item at a time, we send an extracted markdown file to Aristotle, along with the --context of all the previous Lean files.
8. Claude then reads Aristotle's output, and decides whether this counts as "attention needed", "statement formalized", or "proof formalized". It copies both the extracted markdown (as a module doc) and Aristotle's proof into file, ready for providing as context for the next run. It also does some minor cleanup (e.g. renaming duplicate theorem part_i; it could also do stylistic cleanup like expanding exact? but I haven't bothered).

Oh, impressive automatic work!

[Yoh Tanimoto]

I tried to send a small lemma in my own paper (Lemma A.2 in https://arxiv.org/abs/2403.09800) in LaTeX to Aristotle, and after some trials it seems that I got a right result. I'm quite impressed!

1. I first sent a LaTeX file, and got a wrong formalization ("for sufficiently large M..." was translated into "there exists M...")
2. I corrected the generated .lean file and asked Aristotle to fill in sorry, but it failed.
3. I sent again the corrected .lean file with the instruction to follow the proof of the LaTeX file, still failed.
4. Then I explicitly wrote the statement in LaTeX file in the form "There is M_0 such that for all M, M_0 < M,..." and then sent it to Aristotle and got the right statement and a proof.

Except that there is one line (line 166) where the infoview says "aesop: failed to prove the goal after exhaustive search.", but #print axioms says that it does not depend on sorryAx. How should I understand this message?

(I slightly edited the generated file because a small part was broken, but it was easy to fix)

/-

This file was generated by Aristotle.

Lean version: leanprover/lean4:v4.24.0
Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
This project request had uuid: ddb4d558-7106-4a48-8b3b-8e3ece474d04
-/

/-

Formalization of short range localizing functions and Lemma 1.2 from the provided LaTeX snippet.
We define the structure `IsShortRangeLocalizing` capturing the properties (i)-(v) of short range localizing functions.
We then state and prove `lemma_1_2`, which asserts a scaling property for the function `b` associated with a short range localizing function `a`.
The proof relies on the decay property of `b` and the finiteness of integer points in bounded balls.
-/

import Mathlib

set_option linter.mathlibStandardSet false

open scoped BigOperators
open scoped Real
open scoped Nat
open scoped Classical
open scoped Pointwise

set_option maxHeartbeats 0
set_option maxRecDepth 4000
set_option synthInstance.maxHeartbeats 20000
set_option synthInstance.maxSize 128

set_option relaxedAutoImplicit false
set_option autoImplicit false

noncomputable section

/-
Checking definitions of EuclideanSpace and PiLp.
-/

#check EuclideanSpace
#check PiLp

/-
Definitions of short range localizing functions and related concepts.
-/

open Real

abbrev Rd (d : ℕ) := EuclideanSpace ℝ (Fin d)
abbrev Zd (d : ℕ) := Fin d → ℤ

def toRd (d : ℕ) (z : Zd d) : Rd d :=
  (EuclideanSpace.equiv (Fin d) ℝ).symm (fun i => (z i : ℝ))

instance (d : ℕ) : Coe (Zd d) (Rd d) where
  coe := toRd d

def b_func (d : ℕ) (δ : ℝ) (a : Rd d → ℝ) (x : Rd d) : ℝ :=
  (1 + ‖x‖) ^ ((d : ℝ) + δ) * a x

def discreteConvolution (d : ℕ) (f g : Rd d → ℝ) (x : Rd d) : ℝ :=
  ∑' y : Zd d, f (x - (y : Rd d)) * g (y : Rd d)

def iteratedConvolution (d : ℕ) (f : Rd d → ℝ) : ℕ → Rd d → ℝ
| 0 => fun _ => 0
| 1 => f
| (n + 1) => discreteConvolution d f (iteratedConvolution d f n)

structure IsShortRangeLocalizing (d : ℕ) (δ : ℝ) (a : Rd d → ℝ) : Prop where
  pos : ∀ x, 0 < a x
  decay : ∃ c_δ ≥ 0, ∀ x, a x ≤ c_δ * (1 + ‖x‖) ^ (-2 * ((d : ℝ) + δ))
  regularity : ∃ K, ∀ x, ∀ y : Rd d, ‖y‖ ≤ 2 * Real.sqrt (d : ℝ) →
    b_func d δ a (x + y) / b_func d δ a x ≤ K
  convolution_bound : ∃ c, ∃ ε > 0, ∀ n ≥ 1, ∀ x,
    iteratedConvolution d (b_func d δ a) n x ≤ c ^ n * b_func d δ a (ε • x)
  eventually_decreasing : ∃ M₀, ∀ x x', M₀ ≤ ‖x‖ → ‖x‖ ≤ ‖x'‖ →
    b_func d δ a x' ≤ b_func d δ a x

/-
The function b(x) tends to 0 as |x| tends to infinity.
-/

theorem lemma_b_tendsto_zero (d : ℕ) (δ : ℝ) (a : Rd d → ℝ) (h : IsShortRangeLocalizing d δ a) (hδ : 0 < δ) :
    Filter.Tendsto (b_func d δ a) (Filter.cocompact (Rd d)) (nhds 0) :=
by
-- From property (ii), a(x) ≤ c_δ * (1 + |x|)^(-2(d+δ)).
  obtain ⟨c_δ, hc_δ⟩ : ∃ c_δ ≥ 0, ∀ x, a x ≤ c_δ * (1 + ‖x‖) ^ (-2 * ((d : ℝ) + δ)) := by
    exact h.decay;
-- Using the inequality from property (ii), we can bound the expression.
  have h_bound : ∀ x, (1 + ‖x‖) ^ ((d : ℝ) + δ) * a x ≤ c_δ * (1 + ‖x‖) ^ (-((d : ℝ) + δ)) := by
    intro x; convert mul_le_mul_of_nonneg_left ( hc_δ.2 x ) ( Real.rpow_nonneg ( by positivity : 0 ≤ 1 + ‖x‖ ) ( ( d : ℝ ) + δ ) ) using 1 ; ring;
    rw [ mul_assoc, ← Real.rpow_add ( by positivity ) ] ; ring;
-- Since $(1 + ‖x‖)^{-((d : ℝ) + δ)}$ tends to $0$ as $‖x‖$ tends to infinity, the product also tends to $0$.
  have h_lim_zero : Filter.Tendsto (fun x : Rd d => (1 + ‖x‖) ^ (-((d : ℝ) + δ))) (Filter.cocompact (Rd d)) (nhds 0) := by
    simpa using tendsto_rpow_neg_atTop ( by positivity : 0 < ( d : ℝ ) + δ ) |> Filter.Tendsto.comp <|
    tendsto_const_nhds.add_atTop <| tendsto_norm_cocompact_atTop;
  exact squeeze_zero ( fun x => mul_nonneg ( Real.rpow_nonneg ( by positivity ) _ ) ( h.pos x |> le_of_lt ) )
    h_bound ( by simpa using h_lim_zero.const_mul c_δ )

/-
The set of integer points in Z^d with Euclidean norm bounded by R is finite.
-/

theorem lemma_finite_ball_Zd (d : ℕ) (R : ℝ) : {x : Zd d | ‖(x : Rd d)‖ ≤ R}.Finite := by
-- Each coordinate i of x is bounded by R, so x i is in the finite set of integers in [-R, R].
  have h_bounded : ∀ x : Zd d, ‖toRd d x‖ ≤ R → ∀ i : Fin d, abs (x i) ≤ R := by
    intro x hx i; specialize hx; have := hx; simp_all +decide [ EuclideanSpace.norm_eq ];
    exact le_trans ( Real.abs_le_sqrt <| Finset.single_le_sum ( fun i _ => sq_nonneg <| toRd d x i ) <|
      Finset.mem_univ i ) hx;
-- Therefore, for each coordinate i, x i is bounded by ⌊R⌋, so there are only finitely many possible values for x.
  have h_finite_bound : ∀ x : Zd d, ‖toRd d x‖ ≤ R → ∀ i : Fin d, abs (x i) ≤ ⌈R⌉₊ := by
    exact fun x hx i => by exact_mod_cast le_trans ( h_bounded x hx i ) ( Nat.le_ceil _ ) ;
  exact Set.Finite.subset ( Set.finite_Icc _ _ ) fun x hx => ⟨ fun i => neg_le_of_abs_le <| h_finite_bound x hx i, fun i => le_of_abs_le <| h_finite_bound x hx i ⟩

/-
Lemma 1.2: Let b be as in Definition 1.1. Then, there is 0 < M such that, for all M_tilde in N with M < M_tilde we have b(M_tilde x / 3) <= b(x), x in Z^d.
-/

theorem lemma_1_2 (d : ℕ) (δ : ℝ) (a : Rd d → ℝ) (h : IsShortRangeLocalizing d δ a) (hδ : 0 < δ) :
    ∃ M > 0, ∀ M_tilde : ℕ, M < M_tilde → ∀ x : Zd d, b_func d δ a (((M_tilde : ℝ) / 3) • (x : Rd d)) ≤ b_func d δ a x :=
by
-- By property (v) of IsShortRangeLocalizing, there is an M0 such that b is decreasing for ‖x‖ ≥ M0.
  obtain ⟨M0, hM0⟩ : ∃ M0 ≥ 0, ∀ x x', M0 ≤ ‖x‖ → ‖x‖ ≤ ‖x'‖ → b_func d δ a x' ≤ b_func d δ a x := by
    cases' h.eventually_decreasing with M₀ hM₀;
    exact ⟨ Max.max M₀ 0, le_max_right _ _, fun x x' hx hx' => hM₀ x x' ( le_trans ( le_max_left _ _ ) hx ) hx' ⟩;
-- For |x| >= 3M0, we have |(M_tilde/3)x| = (M_tilde/3)|x| >= (M/3)|x| >= |x| if M >= 3.
  obtain ⟨M1, hM1⟩ : ∃ M1 ≥ 3, ∀ M_tilde : ℕ, M1 ≤ M_tilde → ∀ x : Zd d, ‖(toRd d x)‖ ≥ 3 * M0 → b_func d δ a ((M_tilde / 3 : ℝ) • toRd d x) ≤ b_func d δ a (toRd d x) := by
    refine' ⟨ 3, by norm_num, fun M_tilde hM_tilde x hx => hM0.2 _ _ _ _ ⟩;
    · linarith;
    · rw [ norm_smul, Real.norm_of_nonneg ( by positivity ) ] ; nlinarith [ show ( M_tilde : ℝ ) ≥ 3 by norm_cast ];
-- For x in S with x != 0, b(x) > 0 by property (i).
  obtain ⟨M2, hM2⟩ : ∃ M2 ≥ M1, ∀ x : Zd d, ‖(toRd d x)‖ ≤ 3 * M0 → x ≠ 0 → ∀ M_tilde : ℕ, M2 ≤ M_tilde → b_func d δ a ((M_tilde / 3 : ℝ) • toRd d x) ≤ b_func d δ a (toRd d x) := by
-- For x in S with x != 0, b(x) > 0 by property (i). Since b(y) -> 0 as |y| -> infinity (lemma_b_tendsto_zero), for each x in S, there exists Mx such that for all M_tilde > Mx, b((M_tilde/3)x) <= b(x).
    have hMx : ∀ x : Zd d, ‖(toRd d x)‖ ≤ 3 * M0 → x ≠ 0 → ∃ Mx : ℕ, ∀ M_tilde : ℕ, Mx ≤ M_tilde → b_func d δ a ((M_tilde / 3 : ℝ) • toRd d x) ≤ b_func d δ a (toRd d x) := by
      intros x hx hx_ne_zero
      have h_lim : Filter.Tendsto (fun M_tilde : ℕ => b_func d δ a ((M_tilde / 3 : ℝ) • toRd d x)) Filter.atTop (nhds 0) := by
        have h_lim : Filter.Tendsto (fun y : Rd d => b_func d δ a y) (Filter.cocompact (Rd d)) (nhds 0) := by
           exact?;
        refine' h_lim.comp _;
        have h_lim : Filter.Tendsto (fun M_tilde : ℕ => ‖((M_tilde / 3 : ℝ) • toRd d x)‖) Filter.atTop Filter.atTop := by
          norm_num [ norm_smul ];
          apply Filter.Tendsto.atTop_mul_const
          apply norm_pos_iff.mpr
          rw [toRd]
          simp only [PiLp.continuousLinearEquiv_symm_apply, ne_eq, WithLp.toLp_eq_zero]
          by_contra! hxzero
          apply hx_ne_zero
          ext i
          simp only [Pi.zero_apply]
          have : x i = (0 : ℝ) := by
            rw [funext_iff] at hxzero
            exact hxzero i
          simp only [Int.cast_eq_zero] at this
          exact this
          exact tendsto_natCast_atTop_atTop.atTop_div_const zero_lt_three
        norm_num +zetaDelta at *;
        convert h_lim using 1;
        exact?;
      have := h_lim.eventually ( ge_mem_nhds <| show 0 < b_func d δ a ( toRd d x ) from mul_pos ( Real.rpow_pos_of_pos ( add_pos_of_pos_of_nonneg zero_lt_one <| norm_nonneg _ ) _ ) <| h.pos _ ) ; aesop;
    choose! Mx hMx using hMx;
    have := lemma_finite_ball_Zd d ( 3 * M0 );
    exact ⟨ Max.max M1 ( Finset.sup ( this.toFinset ) Mx ), le_max_left _ _, fun x hx hx' M_tilde hM_tilde => hMx x hx hx' M_tilde ( le_trans ( Finset.le_sup ( f := Mx ) ( this.mem_toFinset.mpr hx ) ) ( le_trans ( le_max_right _ _ ) hM_tilde ) ) ⟩;
  use M2 + 1;
  bound;  -- aesop: failed to prove the goal after exhaustive search."
  by_cases hx : x = 0 <;> simp_all +decide;
  · unfold b_func; norm_num [ toRd ] ;
    erw [ WithLp.toLp_zero ] ; norm_num;
  · by_cases hx' : ‖toRd d x‖ ≤ 3 * M0;
    · exact right_2 x hx' hx M_tilde ( by linarith );
    · exact right_1 M_tilde ( by linarith ) x ( by linarith )

#print axioms lemma_1_2

[Vlad Tsyrklevich]

Yoh Tanimoto said:

Except that there is one line (line 166) where the infoview says "aesop: failed to prove the goal after exhaustive search.", but #print axioms says that it does not depend on sorryAx. How should I understand this message?

aesop is normally a finishing tactic. In this case it ran and modified the goal state but didn't manage to finish the goal, but Aristotle managed to close the goal afterwards. So the proof is technically correct (e.g. no sorryAx) but bad style (prone to breaking if the aesop rule set changes.)

[Yoh Tanimoto]

Vlad Tsyrklevich said:

aesop is normally a finishing tactic. In this case it ran and modified the goal state but didn't manage to finish the goal

I see, thanks! I think I understood what aesop did here and could remove the warning.

[Yoh Tanimoto]

What is the best way in this case? 4. worked, while I hope that there is a way to send a .lean file with suggestions for proof, but 3. did not work.

1. I first sent a LaTeX file, and got a wrong formalization ("for sufficiently large M..." was translated into "there exists M...")
2. I corrected the generated .lean file and asked Aristotle to fill in sorry, but it failed.
3. I sent again the corrected .lean file with the instruction to follow the proof of the LaTeX file, still failed.
4. Then I explicitly wrote the statement in LaTeX file in the form "There is M_0 such that for all M, M_0 < M,..." and then sent it to Aristotle and got the right statement and a proof.

[Nick_adfor]

Vlad Tsyrklevich said:

Yoh Tanimoto said:

Except that there is one line (line 166) where the infoview says "aesop: failed to prove the goal after exhaustive search.", but #print axioms says that it does not depend on sorryAx. How should I understand this message?

aesop is normally a finishing tactic. In this case it ran and modified the goal state but didn't manage to finish the goal, but Aristotle managed to close the goal afterwards. So the proof is technically correct (e.g. no sorryAx) but bad style (prone to breaking if the aesop rule set changes.)

So how can we fix the bad style?

[Yoh Tanimoto]

Nick_adfor said:

So how can we fix the bad style?

I'm not sure whether this is the canonical way, but you can see what aesop does by writing show_term.
In this case,

  refine ⟨?_, ?_⟩
  · linarith
  · intro M_tilde hM_tilde x

and below you can copy the remaining argument in the second block, up to renaming automatically generated .right assumptions.

[Kim Morrison]

aesop?

[Nick_adfor]

Alex Meiburg said:

Nick_adfor said:

Also there's nothing like bound?

I have a PR for this actually, I admit the PR was mostly motivated by my own wanting to have this to improve Aristotle's outputs: #27262 (I haven't had time to touch it in a while)

But at the moment you can just do

aesop? (rule_sets := [Bound, -default]) (config := Mathlib.Tactic.Bound.boundConfig)

which is exactly equivalent to calling bound, with aesop?'s proof script generation.

I can say that this really helps!

[Nick_adfor]

The reason I want to cut "bound" is because of "bound" will forbid me from using "#min_imports". But now I find that "induction'" and "Unknown identifier fun₀" forbids me using "#min_imports"......

[Nick_adfor]

Kim Morrison said:

aesop?

I can say that <;> aesop? gives [apply this] but it will fail.

[Nick_adfor]

Yoh Tanimoto said:

Nick_adfor said:

So how can we fix the bad style?

I'm not sure whether this is the canonical way, but you can see what aesop does by writing show_term.
In this case,

  refine ⟨?_, ?_⟩
  · linarith
  · intro M_tilde hM_tilde x

and below you can copy the remaining argument in the second block, up to renaming automatically generated .right assumptions.

<;> show_term aesop cannot work too.

[Nick_adfor]

<;> aesop means that aesop is used in every goal, but can aesop? give something that can be used in every goal?

[Nick_adfor]

Aristotle will generate other things after aesop. But what are other things do after <;> aesop?

      have h_total_degree : ∀ (s : Multiset (MvPolynomial (Fin (k + 1)) (ZMod p))), (∀ p ∈ s, p.totalDegree = 1) → s.prod.totalDegree = s.card := by
        intro s a
        subst hE_card
        induction s using Multiset.induction <;> aesop
        -- Apply the lemma that the total degree of a product is the sum of the total degrees, given that both factors are non-zero.
        have h_total_degree_mul : ∀ (f g : MvPolynomial (Fin (k + 1)) (ZMod p)), f ≠ 0 → g ≠ 0 → (f * g).totalDegree = f.totalDegree + g.totalDegree := by
          exact fun f g a a_3 => totalDegree_mul_of_isDomain a a_3
        by_cases h : a_1 = 0 <;> by_cases h' : s.prod = 0 <;> simp_all +decide [add_comm]
        rw [eq_comm] at a_2
        simp_all only [Multiset.card_eq_zero, Multiset.notMem_zero, IsEmpty.forall_iff, implies_true]

[Nick_adfor]

And for this part, aesop generate a new identifier "a" that aesop? show only "simp only" but cannot give "a"

            have h_deg_j : (elimination_polynomials A i).degreeOf j = 0 := by
              unfold elimination_polynomials
              induction' (A i) using Finset.induction <;> aesop
              · norm_num [MvPolynomial.degreeOf]
              · -- Since $j \neq i$, the degree of $X_i - C a$ in $j$ is zero.
                have h_deg_j_zero : MvPolynomial.degreeOf j (MvPolynomial.X i - MvPolynomial.C a) = 0 := by

[Yoh Tanimoto]

Nick_adfor said:

<;> show_term aesop cannot work too.

show_term bound; worked with me, in the sense that the term was showing that I had to use either refine or constructor, the next goal was closed by bound or linarith, and then I wrote intro, etc.

[Yoh Tanimoto]

Kim Morrison said:

aesop?

I replaced bound by aesop? and it is taking more than 5 minutes to compile. why is that?

[Nick_adfor]

So till now we know nothing about aesop :( I mean that even we can check its origin code, we cannot explain what happened to aesop to make it so strange.

[Nick_adfor]

I was trying a very silly way: replace "aesop" with "aesop?" one by one and check if the [apply] can work.

[Nick_adfor]

If it can, then replace. If it cannot, then paste it here. But it may be nothing connecting with Aristotle now. I'm wondering which part should we make some change to solve the problem thoroughly? Aristotle or aesop?

[Jakob von Raumer]

@Nick_adfor I would first resolve the <;> into individual calls before starting to resolve the aesop call.

[Nick_adfor]

Hi,

Aristotle ran into an unexpected issue while processing your project. In most cases, retrying the project will resolve the issue. Thank you for your understanding, and please feel free to reply to this email if the issue persists.

Sincerely,
The Aristotle Team

[Nick_adfor]

Jakob von Raumer said:

Nick_adfor I would first resolve the <;> into individual calls before starting to resolve the aesop call.

I'm wondering why
<;> aesop
is not equal to
· aesop
· aesop
· aesop
...

[Eric Wieser]

and please feel free to reply to this email if the issue persists.

This thread is presumably not a substitute for sending emails

[Eric Wieser]

I'm wondering why

Can you reduce this to a #mwe, and then ask it in a new thread? This thread is probably also not the best place to discuss the workings of aesop

[Kim Morrison]

Nick_adfor said:

Jakob von Raumer said:

Nick_adfor I would first resolve the <;> into individual calls before starting to resolve the aesop call.

I'm wondering why
<;> aesop
is not equal to
· aesop
· aesop
· aesop
...

@Nick_adfor, I have been noticing recently that you are writing many low effort posts, where it seems you have put insufficient effort into understanding or solving the problem yourself before asking. (See immediately above for examples, but there are many others.) Can you please think about how to improve this before continuing to use the leanprover Zulip?

[Nick_adfor]

Kim Morrison said:

Nick_adfor said:

Jakob von Raumer said:

Nick_adfor I would first resolve the <;> into individual calls before starting to resolve the aesop call.

I'm wondering why
<;> aesop
is not equal to
· aesop
· aesop
· aesop
...

@Nick_adfor, I have been noticing recently that you are writing many low effort posts, where it seems you have put insufficient effort into understanding or solving the problem yourself before asking. (See immediately above for examples, but there are many others.) Can you please think about how to improve this before continuing to use the leanprover Zulip?

First, there is currently no bound? We need to use:

aesop? (rule_sets := [Bound, -default]) (config := Mathlib.Tactic.Bound.boundConfig)

Second, <;> aesop? cannot be used when followed by other proofs afterward. It seems to allow generating new variables for subsequent calls.

Third, <;> aesop
is not equal to
· aesop
· aesop
· aesop
...

The above issues are related to aesop. These problems occur because Aristotle adopts this style of coding. Perhaps we should move this discussion to the aesop section. This behavior of aesop is not documented in the technical materials I have found.

Similar stylistic issues exist with simp + delta. I often remove delta, and it still works fine.

Additionally, aristotle ran into an unexpected issue while processing the project. This is all I know. This seems a temporary error. Even when I try it twice it will disappear.

[Jireh Loreaux]

Kim Morrison said:

Can you please think about how to improve this before continuing to use the leanprover Zulip?

@Nick_adfor please pay attention to this.

[Nick_adfor]

About Aristotle's coding style.lean

[Nick_adfor]

The whole code is here:
https://github.com/NickAdfor/The-polynomial-method-and-restricted-sums-of-congruence-classes/blob/main/%E5%A6%88%E5%92%AA%E6%B2%B3%E7%A7%BB%E4%BD%8D%20with%20trial%20to%20cut%20aesop.lean

[Nick_adfor]

Kim Morrison said:

before continuing to use the leanprover Zulip?

Kim, before continuing to use the leanprover Zulip, we used Wechat to develop code, where people talked in Chinese. We all notice that here is Discussion thread for Aristotle API. In fact I've not the necessity to publish the code in Mathlib version (min_imports, cut aesop, not more maxHeartbeats) but make all of the community members accept code in an Aristotle way. But as there's already a Cauchy-Davenport Theory in Mathlib, add another proof of it is better.

[Gavin Zhao]

Nick, Zulip is different from WeChat groups. You can't be bringing the habit of chatting in WeChat to discussions on Zulip. People's times are precious, so your post must go straight to the problem you're trying to get help with. Zulip is not a place for you to dump your stream of thoughts into.

[Gavin Zhao]

DM me if you're confused.

[Nick_adfor]

Yet anyway, posting Aristotle style problems or debating for community difference are all easier than solving the problem. I should say that it's not hard for me as a coder to adapt to Aristotle style, it's just a little more "aesop". But what will happen when I try to get it understandable for mathematical use? For code in Mathlib, I've never seen too more "aesop". I may think "aesop" in code is the same as "The proof is trivial" in math, which represents signal impressive work, but also comes across as overly dense and almost bulldozing in their brevity.

[Nick_adfor]

Proposing an Aristotle-style change or an aesop update might introduce too many dependencies, making it impractical to complete nowadays. That’s why I chose to limit aesop in a rather naïve way: by using aesop?. For the failing parts—like the ones I've posted here—I further pull requests to aesop itself, since the issue lies with aesop's handling, not with Aristotle's.

[Artie Khovanov]

@Nick_adfor if you would like to suggest a concrete change to Aesop, please make a new thread suggesting that change, with a justification. Bear in mind that Aesop is designed to be a white-box automation tool and is not being optimised for usability by AI systems.

[Jireh Loreaux]

Nick, there's no rule not to use aesop in Mathlib. In fact, the category theory end of the library uses (a slight variant of) aesop all over the place, but behind the scenes as an autoparam. The only reason one might not want to use aesop is performance.

[Artie Khovanov]

Indeed aesop is used extensively in Mathlib anywhere where somebody has taken the time to curate a ruleset. And yeah it's very useful as an autoparam.

[Yaël Dillies]

Jireh Loreaux said:

Nick, there's no rule not to use aesop in Mathlib. In fact, the category theory end of the library uses (a slight variant of) aesop all over the place, but behind the scenes as an autoparam. The only reason one might not want to use aesop is performance.

Does it? I thought cat_disch now uses grind under the hood?

[Chris Henson]

I see a few files have set_option mathlib.tactic.category.grind true, but I think aesop is the default otherwise?

[Lawrence Wu (llllvvuu)]

EDIT: We just pushed a change to make Aristotle not use non-terminal aesop, so the following workaround should no longer be needed.

For now, there is a workaround that can be used to avoid non-terminal aesop. This is not an announcement of an official solution.

You can modify tactic behavior via imported files, but not inside the file you're working in directly (due to a bug on our end currently this will cause Aristotle errors). So:

1. Create a file, e.g. TerminalAesop.lean, that says:

import Mathlib.Tactic.Bound

namespace HarmonicLean.Aesop
syntax (name := harmonicAesop) "aesop" : tactic
macro_rules (kind := harmonicAesop) | `(tactic| aesop) => `(tactic| aesop (config := {terminal := true}))
syntax (name := harmonicBound) "bound" : tactic
open Mathlib.Tactic in
macro_rules (kind := harmonicBound) | `(tactic| bound) => `(tactic| aesop (rule_sets := [Bound, -default]) (config := Bound.boundConfig) (config := {terminal := true}))
end HarmonicLean.Aesop

2.
a. If you have a Lean file you're working in, you can add import TerminalAesop there
b. If you don't have a Lean file you're working in, you can put under "Optional: Attach a Lean file as context" a file with the following contents:

import Mathlib
import TerminalAesop

set_option linter.mathlibStandardSet false

open scoped BigOperators
open scoped Real
open scoped Nat
open scoped Classical
open scoped Pointwise

set_option maxHeartbeats 0
set_option maxRecDepth 4000
set_option synthInstance.maxHeartbeats 20000
set_option synthInstance.maxSize 128

set_option relaxedAutoImplicit false
set_option autoImplicit false

noncomputable section

This technique is generalizable to constrain Aristotle's behavior, though we cannot guarantee that Aristotle will perform well in all possible configurations (this terminal aesop configuration is the only one we tested and found works well).

[Alex Meiburg]

There are two other versions of this that people might find useful, especially if they're working for mathlib:

• "Overwrite" native_decide to be an alias for decide +kernel. This will naturally stop Aristotle from doing lots of "brute force" calculations; you can then replace native_decide with decide +kernel in the produced proofs and it should behave just as otherwise.
• You can overwrite nlinarith to be linarith. I know that some people feel that nlinarith proofs can be a bit ugly - just a bit bag of facts without much mathematical motivation. Sometimes.

Also - no guarantees, and recognize this may very well hurt proving ability! But it's a way to shape the style of proofs you get, somewhat. :)

[Nick_adfor]

The reason I want to cut aesop is maxHeartbeats. I think that to raise maxHeartbeats may cause the code run slow.

[Nick_adfor]

For bound, it will forbid me from using min_imports. So does induction'

[Nick_adfor]

Artie Khovanov said:

Nick_adfor if you would like to suggest a concrete change to Aesop, please make a new thread suggesting that change, with a justification. Bear in mind that Aesop is designed to be a white-box automation tool and is not being optimised for usability by AI systems.

I try to understand the concept of “white-box” through reading related articles. The most recent one I read was Tactic Script Optimisation for aesop, which introduces a solution to the previous problem for aesop's “non-depth-first, structurally disorganized, and non-idiomatic.” However, at the time that paper was written, there was no Aristotle AI. Aristotle adopt a result-driven approach to proof automation, prioritizing the completion of a proof at all costs. As a result, its calls to aesop become unnecessarily frequent, which may increase the automated search time and also make the proofs harder for humans to follow. Maybe that makes aesop back to a “non-depth-first, structurally disorganized, and non-idiomatic” way...

[Artie Khovanov]

Yes, I agree the combination of a precisely calibrated white box automation tool with a RL-trained stochastic system leads to difficult to read proofs. A human in this situation would simply add or amend the Aesop tags around the theory they are working on to improve code quality and reusability. But I mean, why are you expecting Aristotle to produce idiomatic code? That's not what it's designed to do. Unfortunately for now proofs must be cleaned up by hand. Perhaps in the future there will be AI tools with different training objectives.

[Nick_adfor]

Yes, I'm try to "amend the Aesop tags around the theory working on". Actually, I cannot write something like above namespace HarmonicLean.Aesop. There's more to learn to adapt to Aristotle's output

[Lawrence Wu (llllvvuu)]

We just pushed a change to make Aristotle not use non-terminal aesop, so the above workaround should no longer be needed.

[Eric Rodriguez]

Do let us know if you notice any code quality differences - it's super interesting to hear you guys' takes.