confidence in peer review

Stream: general

[Miguel Raz Guzmán Macedo]

@Kevin Buzzard , thank you for all the help on the previous stream - I wanted to pick your brain for second.

I just read your talk from Pittsburgh on the many examples for ... unencouraging non-retractions of peer reviewed mathematics.

Is anyone already placing beers on any given fields of maths that will fail to be formally verified?

[Johan Commelin]

I'm not aware of such a bet

[Kevin Buzzard]

Most maths is absolutely fine. When I give talks like that in maths departments I try and wind people up and suggest that maths is on the verge of collapse, but the truth is that humans know what they're doing and 99% of it could in theory be formally verified, except that it would take thousands of years to do it

[Miguel Raz Guzmán Macedo]

At the end of your presentation, you mentioned confidence in a handful of results - but it seems to me one can extend a much less charitable interpretation of many results given unaligned interests of academia, peer review, and formal verification.

[Mario Carneiro]

thousands of years is a gross overestimate. Several years and millions of people is more accurate

[Kevin Buzzard]

There will be incomplete proofs, and proofs where the missing arguments are "known to the experts" and I am concerned that one day when the experts are gone this will translate to "known to nobody". The arrogance of our community is that we believe that by the time they're gone, we will know new and better ways to prove the results for which the proofs died.

[Mario Carneiro]

or at least a decent percentage of the people actually producing the papers

[Marc Huisinga]

i believe that verifying a great deal of computational complexity theory will be very difficult, i haven't found any prior work in a quick search either.
i don't think that it will be difficult because stuff is wrong, but because the arguments and proofs are the way they are.

[Kevin Buzzard]

Yes, thousands of person-years is what I meant.

[Miguel Raz Guzmán Macedo]

Kevin Buzzard said:

Most maths is absolutely fine. When I give talks like that in maths departments I try and wind people up and suggest that maths is on the verge of collapse, but the truth is that humans know what they're doing and 99% of it could in theory be formally verified, except that it would take thousands of years to do it

Well, a lot of institutions and brilliant people have believed ridiculous things, especially when they only need the approval of each other at the end of the day.

[Miguel Raz Guzmán Macedo]

To clarify, I'm not being a catastrophist either, but I do feel some inclination to hear out more of those arguments now.

[Miguel Raz Guzmán Macedo]

Kevin Buzzard said:

There will be incomplete proofs, and proofs where the missing arguments are "known to the experts" and I am concerned that one day when the experts are gone this will translate to "known to nobody". The arrogance of our community is that we believe that by the time they're gone, we will know new and better ways to prove the results for which the proofs died.

How easy is it for you to look at a lean proof someone else made and be able to write it own on pencil and paper, rigorously?

[Miguel Raz Guzmán Macedo]

I guess I am also asking for the Lean community in general.

[Kevin Buzzard]

Depends on whether it's a tactic or term mode proof.

[Reid Barton]

often the easiest way is ignore the Lean proof and just notice that the statement is true

[Kevin Buzzard]

Also depends on what you mean by "rigorously". Some files like data.finset are exactly how Reid is describing. All the theorems in there can be proved by "duh, it's a trivial result about a finite set". Hence all the theorems in the other files which use those theorems -- you don't have to justify why the use is OK and no mathematician would complain. However at the top end of mathematics you have people writing down arguments which contain hugely general statements which experts understand can be justified and such people would argue until they're blue in the face that the arguments were rigorous. So your question isn't really well-defined. Rigour is in the eye of the beholder. Lean is just one example of a beholder.

[Bryan Gin-ge Chen]

Along the same lines as what Reid and Kevin are saying, there are often many Lean statements that should simply be ignored from the point of view of pencil + paper math. (Maybe we should think about adding a "hiding" feature to the mathlib docs?)

[Kevin Buzzard]

I think that things like extensionality lemmas have an important role to play in the documentation. You can understand Lean's conventions with ext and ext_iff if you can see them. But every one of them should be ignored from the point of view of pencil and paper maths.

[Miguel Raz Guzmán Macedo]

Thanks for the input!