Kaiyu Yang

Several thousands of these warnings are expected. Most of them are because in Lean one can define things using macros such as [`to_additive`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/ToAdditive/Frontend.html). These definitions are not traced by LeanDojo.

random

Thanks for these PRs! I'll take a look when I get a chance.

Maybe try the latest `main` branch? This is the output I got: ``` (lean-dojo) kaiyuy@learnfair6006:~$ VERBOSE=1 ipython Python 3.12.9 | packaged by Anaconda, Inc. | (main, Feb 6 2025, 18:56:27)...

This is due to recent changes in Lean. I just fixed it in the current `main` branch (please try) and will release a new LeanDojo version after running some unittests.

Hi, As discussed in the LeanEuclid paper, it implements a variant of Avigad's system E, so there may be some discrepancies in the axioms. Also, `intersection_circles` is actually correct even...

The code example is not runnable. I can take a look if you have a minimal runnable example to reproduce the error. Usually the "Cannot find the *.ast.json file" error...

Re > Another thing, how could we `dojo.run_tac()` on multiple tactics or single line contain `;`? Some seems to work while other doesn't. > > Example: > > 1. theorem...

LeanDojo cannot be used to interact with theorems from the Lean 4 repo itself. See https://leandojo.readthedocs.io/en/latest/limitations.html#limitations

The `classical` in `classical rw [map_eq_image]; exact nsmul_piAntidiag _ _ hn` is a scoping tactic (see https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md#classical). It's equivalent to `classical (rw [map_eq_image]; exact nsmul_piAntidiag _ _ hn)` and should...