[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?

[g15jv2dp]

Yes, they get grants to work on it. Other questions? I can't say I enjoy this "gotcha" tone.

[a_wild_dandan]

Snark and contrarianism are specialties around here. Thank you for sharing your experience; I genuinely appreciate it.

[GPerson]

The person you are replying to asked a very useful question, and you supplied a useful answer. I don’t detect any snarky tone in their comment.

[raincole]

It sounds quite "gotcha" to me.

Compare these two cases:

> 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?

> people who use or contribute to lean

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

The "And" at the begining makes it snarky to me. It's probably just me tho.

[nickpsecurity]

I’m with them. They’re using a tool they’re paid to work on. That’s always a special case. The general case would be what percentage of mathematicians use (a) proof assistants at all, (b) mechanized proof assistants, and (c) Lean specifically.

Do most working mathematicians use proof assistant or checkers? Does anyone have a percentage with feedback on how they use them?

[TeMPOraL]

> They’re using a tool they’re paid to work on. That’s always a special case.

FWIW, the industry term for this is "dogfooding", and it's usually seen as a predictor of high quality tool.

[nickpsecurity]

There’s two issues here: getting paid to work on a product; using the product yourself. People often do one without much of the other. People dogfooding do both.

For the original question, a survey might want to separate these two. One just says people are working on a product. Why could be any reason, like just making money. People using it, but not paid to, are more valuable as reviewers.

[shakow]

That's not a “gotcha”, but an interrogation on whether what I experienced in bioinformatics (i.e. working on tools, especially already existing ones, is a carreer trap) also applied to maths.

[Jensson]

So they get grants to work on these tools rather than to work on math, seems like a very special situation then and a very special math department and therefore not a good picture for how helpful it is to math departments in general.

[seanhunter]

The mathematicians I know of who work on Lean4 as part of grant-funded research do so because their research funding is for formalising mathematics and Lean4 is the tool they choose to use for that.

I really have no idea why people are taking this approach here.

Proof assistants are useful. People use them to do actual maths. There is a lot of work to formalise all of maths (this isn't a proof assistant thing this is a huge undertaking given maths is 3000+ years old and we've only just decided what formality really fundamentally consists of) so some places you need to do more foundational work than others to make it useful.

[g15jv2dp]

I guess we got in the top 10 worldwide for math in the Shanghai ranking by accident. If you don't know what you're speaking about, sometimes it's wise to not say anything.

[szvsw]

Isn’t working on these tools a form of working on math? Math is a language unto itself.

[nimih]

"No true working mathematician would spend their time using Lean!"

[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