News for hackers. Stuff that matters.

A comment on Formalizing the proof of PFR in Lean4 using Blueprint: a short tour. Parent comment

Re:Formalizing the proof of PFR in Lean4 using Blueprint: a ... by trevyn on Wednesday December 06, 2023 @04:21AM (#38541907)
>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?

[ Parent | on HN ]
Re:Formalizing the proof of PFR in Lean4 using Blueprint: a ... by staunton on Wednesday December 06, 2023 @06:58AM (#38542730)
Here's people who are working on Lean's Mathlib discussing this https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...
[ Parent | on HN ]