Projects: Improve Automation

Stream: ItaLean 2025

[Lorenzo Luccioli]

This thread is dedicated to the Improve Automation project:

• Repository: ?
• Formal Manager: @Jannis Limperg

[Jannis Limperg]

Aesop reference docs (such as they are): https://github.com/leanprover-community/aesop

[Jannis Limperg]

Grind reference: https://lean-lang.org/doc/reference/latest/The--grind--tactic/

[Yoichi Hirai]

I realized that guard constraint of grind_patternisn't yet available in mathlib4:master, which is tied to v4.26.0-rc2. I guess I'll start working with lean4:master. (context: I want lemma val_natCast_of_lt {n a : ℕ} (h : a < n) : (a : ZMod n).val = a around only when the side-condition is known).

[Chris Henson]

Maybe using a nightly toolchain is easier? This should work with Mathlib.

[Yoichi Hirai]

I put

leanprover/lean4:nightly-2025-12-09

in lean-toolchain and ran lake update.

[Yoichi Hirai]

ohh, maybe I need to change the battery version etc

[Yoichi Hirai]

I have a feeling I'm not doing the right thing

**zksecurity@Ubuntu-2404-noble-amd64-base**:**~/mathlib4**$ lake update
**warning:** toolchain not updated; multiple toolchain candidates:

  leanprover/lean4:nightly-2025-12-09

    from mathlib

  leanprover/lean4:v4.26.0-rc2

    from plausible

  leanprover/lean4:v4.25.0-rc1

    from LeanSearchClient

  leanprover/lean4:v4.26.0-rc2

    from importGraph

  leanprover/lean4:v4.26.0-rc2

    from proofwidgets

  leanprover/lean4:v4.26.0-rc2

    from aesop

  leanprover/lean4:v4.26.0-rc2

    from Qq

  leanprover/lean4:v4.26.0-rc2

    from batteries
**info:** mathlib: running post-update hooks

[Chris Henson]

There is a repo https://github.com/leanprover-community/mathlib4-nightly-testing that has the nightly branches. You can check out nightly-testing or a bump/YYYY-MM-DD branch and work from there. You should not have to update the toolchain or lake update yourself.

[Yoichi Hirai]

^ seems to be working (now building). Thank you!

[Chris Henson]

Great! Note that lake exe cache get will still work for these branches as well.

[Farruh Habibullaev]

@Jannis Limperg, as we talked yesterday, here is the pull request for aesop for basic lib - https://github.com/leanprover-community/mathlib4/pull/32682, but it looks like we can't create pull request against the master branch, and I've no idea how to add you as an reviewer as it's disabled.

[Michael Rothgang]

I can do this, and have requested review rom Jannis.

[Farruh Habibullaev]

Thank you!

[Yoichi Hirai]

I'm trying to add a grind_pattern on a lemma mod_eq_of_lt in lean4 repo. The test is not working unless I copy the grind_pattern into the test file. I'm puzzled https://github.com/leanprover/lean4/pull/11584

[Jannis Limperg]

I asked about the question we had yesterday, whether we should be actively replacing manual proofs with automated proofs. TLDR: yes, but only if the manual proof is more than 2-3 lines. Details: #mathlib4 > Policy on replacing manual proofs with automated proofs

This doesn't affect PRs adding annotations -- please make these even if they only save one line. In a bigger proof, they may well enable the automation to make more progress and save more lines.

[Yoichi Hirai]

I need some design decision about grind_pattern. The issue is that I don't want a % b = a when both a and b are values, but I want it when either a or b is not_value. @Leonardo de Moura

Do we want to add disjunction as guard? Is it okay to repeat the grind_pattern?

https://github.com/leanprover/lean4/pull/11584

[Yoichi Hirai]

^ I spoke with Leo offline about this and got an answer.

[Yoichi Hirai]

Is this something interesting to debug

(kernel) application type mismatch
  eq_false_of_decide (eagerReduce (Eq.refl false))
argument has type
  false = false
but function has type
  decide (1 = 0) = false → (1 = 0) = False

on

**Operating system**: Linux (release: 6.8.0-88-generic)
**CPU architecture**: x64
**CPU model**: 32 x AMD Ryzen 9 7950X3D 16-Core Processor
**Available RAM**: 134.24 GB

**VS Code version**: Reasonably up-to-date (version: 1.106.3)
**Lean 4 extension version**: 0.0.221
**Curl installed**: true
**Git installed**: true
**Elan**: Reasonably up-to-date (version: 4.1.2)
**Lean**: Reasonably up-to-date (version: 4.27.0-nightly-2025-12-10)
**Project**: Valid Lean project (path: /home/zksecurity/mathlib4-nightly-testing)
**Active Lean version**: leanprover/lean4-nightly:nightly-2025-12-10 (set by `file:///home/zksecurity/mathlib4-nightly-testing/lean-toolchain`)
**Installed Lean versions**: lean4, lean4-stage0, leanprover/lean4-nightly:nightly-2025-12-09, leanprover/lean4-nightly:nightly-2025-12-10, leanprover/lean4-nightly:nightly-2025-12-11, leanprover/lean4:v4.24.0, leanprover/lean4:v4.25.2, leanprover/lean4:v4.26.0-rc2

observed on https://github.com/pirapira/mathlib4/commit/329354a78e0799c612a01c4701da6ac000ef01dd

[Jannis Limperg]

^ I spoke with Leo offline about this and got an answer.

What was the answer, just out of curiosity?

[Jannis Limperg]

Is this something interesting to debug

Looks like a tactic bug, where a tactic constructs a malformed expression. Definitely interesting.

[Yoichi Hirai]

What was the answer, just out of curiosity?

having this repetition is fine, the overhead is minimal, was the answer.

grind_pattern mod_eq_of_lt => a % b where
  not_value a
  guard a < b

grind_pattern mod_eq_of_lt => a % b where
  not_value b
  guard a < b

[Yoichi Hirai]

a tactic bug

It's caused by grind = annotation on natCast_self. I'll clean up the example and file an issue. https://github.com/pirapira/mathlib4/commit/329354a78e0799c612a01c4701da6ac000ef01dd#diff-045563e9a620ceedb72bba37de77554038dfe9d0ec1bcdc4989585c5020e6b77R147

[Farruh Habibullaev]

I've updated RP with aesop / simp automation - https://github.com/leanprover-community/mathlib4/pull/32698

[Yoichi Hirai]

I pushed a PR for changes that don't require nightly https://github.com/leanprover-community/mathlib4/pull/32776

I have more changes that require guard feature of grind. Shall I wait till guard becomes available in mathlib4 CI?

[Yoichi Hirai]

CI is failing on another lean4 PR because changelog-* tag is missing. Can somebody add this tag?

[Luisa Cicolini]

Yoichi Hirai said:

CI is failing on another lean4 PR because changelog-* tag is missing. Can somebody add this tag?

you usually can add it writing the tag you want (e.g. changelog-library) in the github comments :)

[Yoichi Hirai]

worked! https://github.com/leanprover/lean4/pull/11584#issuecomment-3645387120

[Luisa Cicolini]

dumping some thoughts:

• I spent the last couple days thinking about the lemmas) in Mathlib/Logic/Relation: in particular the lemmas describing the relations between transitive and reflexive closures. The objective would be to make the lemmas about the ReflTransGen (reflexive and transitive closure) grindable.
• The draft above summarizes my failed attempt: the only resulting grindable lemmas were trivial
• However, I came to conclude that the minimal theory for this is already in the file, and we might want to tag for grind all the lemmas in Relation that characterize the relations between ReflGen, TransGen and ReflTransGen. It seems to me that those lemmas are basically (and useful) enough to make more complex reasoning about Relation grindable.

I'd be curious to see if anyone has any thoughts or opinions on this :)

[Riccardo Brasca]

In the quadratic Integers projects we have goals like 4 ∣ 1 - d, knowing that 4 * n = t ^ 2 - d * (2 * B' + 1) ^ 2 and t = 2 * t' + 1 (all the variables are in ℤ). It's easy to use grind to show that -t' ^ 2 - t' + d * B' ^ 2 + d * B' + n works and this is already very nice. Do you think it is possible to make grind guess the element? On paper it is very easy, 4 ∣ 1 - d means that there is k such that 4 * k = 1 - d, and the other relations force k to be what it is.

[Kevin Buzzard]

I don't think grind creates data, I think this has come up before. Just to clarify the issue:

import Mathlib

example (n t d B' t' : ℤ)
    (h1 : 4 * n = t ^ 2 - d * (2 * B' + 1) ^ 2)
    (h2 : t = 2 * t' + 1) :
    4 ∣ 1 - d := by
  -- goes to pencil and paper and multiplies everything out...
  use n - t'^2 - t' + d * (B' + B'^2) -- manually calculated
  grind

[Kevin Buzzard]

It's extra-hard because the solution can't be solved by eliminating d -- you can't just "evaluate (1-d)/4 by subbing in for d", you do need intelligence here to realise that you don't figure out d by dividing by (2B'+1)^2 in h1, you actually need to do something clever. So I'm not even clear what algorithm would be good enough to do this. I think I'm solving this by pattern-spotting -- "oh look there's a 1+4B'+4B'^2, those 4's can help us".

In particular I am not immediately convinced by Riccardo's "the other relations force k to be what it is" -- things like k=(1-(t^2-4n)/(2B'+1)^2)/4 also work algebraically, but the 4's happen not to cancel for this choice.

[Kevin Buzzard]

I asked Claude and it found the factor essentially immediately. This might be a workaround for now!

[Chris Henson]

@Luisa Cicolini I find it very reasonable to annotate Mathlib/Logic/Relation for grind. I have been doing this a bit for the term rewriting project. See this slightly messy diff as an example.

[Luisa Cicolini]

thank you very much! it's very helpful to see how that's used in cslib. I will annotate it and share the result!

[Bhavik Mehta]

Kevin Buzzard said:

I don't think grind creates data, I think this has come up before. Just to clarify the issue:

import Mathlib

example (n t d B' t' : ℤ)
    (h1 : 4 * n = t ^ 2 - d * (2 * B' + 1) ^ 2)
    (h2 : t = 2 * t' + 1) :
    4 ∣ 1 - d := by
  -- goes to pencil and paper and multiplies everything out...
  use n - t'^2 - t' + d * (B' + B'^2) -- manually calculated
  grind

I think this oversimplifies the situation, you can get grind to "create the data" here with less help:

example (n t d B' t' : Int)
    (h1 : 4 * n = t ^ 2 - d * (2 * B' + 1) ^ 2)
    (h2 : t = 2 * t' + 1) :
    4 ∣ 1 - d := by
  subst h2
  grind

But the truth of this example is that we're not really creating data here, instead grind knows enough about the dvd relation to prove it. eg in this case grind knows 4 ∣ 4 * m (inside the lia module). In fact I wonder if it should be solvable without the subst, although I think I understand why it's currently not

[Riccardo Brasca]

Yeah, finding the quotient is what I thought it was the most direct way, but maybe for a tactic it's easier to use properties of dvd.

[Bhavik Mehta]

I wonder if people in this project were thinking about inequalities: #mathlib4 > aesop and inequalities

[Jannis Limperg]

I don't think anyone looked at inequalities specifically. Would have been a good target; I should have thought of that.

[Luisa Cicolini]

I updated the grind annotations after chatting a bit with @Chris Henson and looking at what they're using in cslib. One thing that is not clear to me is what's the preference among the following:

attribute [grind =] reflGen_iff
attribute [grind] ReflGen

and in general thoughts on what is helpful to tag grind in Relation are appreciated :)

[Jannis Limperg]

I hacked together a quick presentation for later:
italean.pptx
Please lmk if you feel misrepresented. :sweat_smile: @Yoichi Hirai @Luisa Cicolini @Farruh Habibullaev @Paul Dietze

[Farruh Habibullaev]

By the way, it's blank, I see no content in the presentation

[Jannis Limperg]

Version where I actually hit the save button:
italean.pptx

[Jannis Limperg]

Do you guys want to do the presentation yourselves?

[Farruh Habibullaev]

I personally prefer you to do it.

[Paul Dietze]

I agree with the statement by @Farruh Habibullaev :)

[Bhavik Mehta]

@Luisa Cicolini your PR is marked as draft, but I think it's basically ready; and it would be nice to have the stuff merged before you all present. Do you want to mark it as ready?

[Luisa Cicolini]

I talked about this a bit with @Jannis Limperg and we were actually working on a refactoring to build the necessary infra around ReflGen and TransGen, so that all the lemmas about ReflTransGen are derived from there (that's why it was drafted). @Jannis Limperg what do you think?

[Jannis Limperg]

This refactoring will take a while, so I'd say let's merge the incremental improvement rather than wait for perfection.

[Luisa Cicolini]

okay! in that case I'm opening it now

[Bhavik Mehta]

have hit merge on it :)

[Luisa Cicolini]

ci did not pass :melt: I will try to fix the issue (and maybe add some grinded theorems, as was also requested)

[Chris Henson]

I mentioned in person, but will write here as well for other's benefit: the error in CI is from MathlibTest/grind/lint.lean. This is a recently added test that checks that grind annotations in Mathlib do not pass a given threshold of instantiations. You can look at the output of that test to see what theorems are the problem and change/remove the annotation. In a few days I believe the next release will also add the ability to add constraints to grind_pattern which can also potentially help.

[Luisa Cicolini]

should be fixed now! EqvGen was understandably the problem

[Bhavik Mehta]

Bhavik Mehta said:

In fact I wonder if it should be solvable without the subst

I convinced myself that this counts as a grind bug, or at least seemingly inconsistent with the docs about grind, so it's reported here: lean4#11631

[Yoichi Hirai]

A different issue I saw in grind use ((kernel) application type mismatch) seems to have disappeared in the nightly build. Minimizing the example was educational though. I saw lots of important type classes.

[Yoichi Hirai]

I started looking for a reviewer for mathlib4#32776 . I also posted in the PR reviews channel. My usual strategy in this phase is gentle persistence.

[Yoichi Hirai]

I got my first PR merged to mathlib. Thank you! I'll continue with more because now grind_pattern can take guard-conditions on mathlib4:master.