11 ms·
>most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math. Is this because the proof author is generally con
by trevyn 3y ago
>most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math.
Is this because the proof author is generally confident that the proof is essentially correct?
- staunton 3y agoHere's people who are working on Lean's Mathlib discussing this https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Array.2EanyM.20is.20inconsistent/near/396178821 https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...