[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!"