Apparently so:
leanprover.zulipchat.com#narrow/chann...

xenaproject.wordpress.com/2025/08/03/a... is a summary of what happened in 2025.

Good question. They're available on my hard drive but Simons never asked for them. I've uploaded them to the Lean Zulip here leanprover.zulipchat.com#narrow/chann...

Of course Barbara! Thanks for asking!

Amongst the projects funded is my project www.renaissancephilanthropy.org/a-dataset-of... to create what in 2025 is a super-hard dataset of pairs (informal hard proof, formal statement) of recent results from top journals. The challenge for machine is to formalise the rest of the paper.

Mathematics is also incomplete (assuming it's consistent) and that hasn't stopped lean from engaging with it at research level

Could you ever envisage lean being useful to verify nontrivial code written in common programming languages or is this asking too much?

I absolutely agree; IPAM is the notable absentee from the list. I organised a conference there in 2023 www.ipam.ucla.edu/programs/wor... bringing together people from mathematics and machine learning and formal methods, and it was a fascinating week!

Lol that was me a few years ago

I did read parts of Langlands document about defining local epsilon factors locally and it was just page after page of representation theory (so it looked like groups acting on vector spaces)

I have never read the algebraic proof of the first inequality in global class field theory, I've just heard that it exists. I read the analytic proof last week though :-) The elementary proof of the prime number theorem still has plenty of basic real analysis in it.