[egl2021]

For now this might be a project for Fields medalists, like Tao and Scholze, who have the leisure to spend 10x the time on a proof. I recently talked to a post-doc in a top-ranked math department, and he doesn't know anyone who actually uses lean4 in their work. For early-career people, it's probably better to trust your intuition and get the papers out.

[g15jv2dp]

I'm a math professor and I know many people who use or contribute to lean. Not all of them are Fields medalists. Maybe it takes more than a couple of people's opinion on the subject to have a good picture.

[shakow]

> people who use or contribute to lean

And do they get tenure- or funding-able output of it, or is it more of a side-hobby?

[flostk]

I'm sure this also depends a lot on the field within mathematics. Areas like mathematical logic or algebra have a pretty formal style anyway, so it's comparatively less effort to translate proofs to lean. I would expect more people from these areas to use proof checkers than say from low-dimensional topology, which has a more "intuitive" style. Of course by "intuitive" I don't mean it's any less rigorous. But a picture proof of some homotopy equivalence is just much harder to translate to something lean can understand than some sequence of inequalities. To add a data point, I'm in geometry/topology and I've never seen or heard of anyone who uses this stuff (so far).

[ocfnash]

If you are curious, I encourage you to look up The Sphere Eversion Project [1].

It was a project in which we formalised a version of Gromov's (open, ample) h-principle for first order differential relations. Part of the reason it was carried out was to demonstrate what is involved formalising something in differential topology.

1. https://leanprover-community.github.io/sphere-eversion/

[enugu]

Pictures can be directly used in formal proofs. See [1] for instance So, the problem is not in principle, but rather, pictures and more direct syntax has not yet been integrated into current proof systems. When that is done, proofs will be much more natural and the formal proof will be closer to the 'proof in the mind'.

[1] https://www.unco.edu/nhs/mathematical-sciences/faculty/mille...

[occamrazor]

For Tao, spending 10x time on aproof still means spending 5x less time than an average postdoc. He is incredibly fast and productive.

[yboris]

lean4 - programming language and theorem prover

https://lean-lang.org/

https://github.com/leanprover/lean4