leanprover-community / leanprover-community/mathlib4
`linarith?/nlinarith?`
Open
@Paul-Lez is already working on this.
Since Jun 4, 2025.
enhancement
help-wanted
please-adopt
t-meta
- Dominant language
- Lean
- Stars
- 4.1k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
Many tactics have a ? version, which functions the same, but provides a hint as to a more specific call to the underlying tactic that the user can make to cause their proof to be more self-contained / performant.
This issue suggests creating linarith? and nlinarith? versions of the linarith and nlinarith tactics respectively.
These would replace the underlying calls with a call to linarith only (or perhaps linear_combination) so that we can avoid very expensive linarith calls in contexts where linarith finds many equations, while making proofs more parseable.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.