3 ms·
Can you give some context on how using Lean benefits? In my understanding, proofs are usually harder to transcribe into Lean which is nobody _writes_ proofs us
by xrisk 2y ago
Can you give some context on how using Lean benefits?
In my understanding, proofs are usually harder to transcribe into Lean which is nobody _writes_ proofs using Lean.
What is a nlinarith?
- llwu 2y agonlinarith is a proof automation that attempts to finish a proof using the simplex method to find a linear combination of hypotheses and things that have already been proven, as well as some quadratic terms of them. Docs: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Linarith/Frontend.html#tacticNlinarith!_ https://leanprover-community.github.io/mathlib4_docs/Mathlib...