Yes exactly! It's easy to get the "divides" ordering confused with the "less or equal to" ordering becase a | b usually implies a <= b. But everything divides zero, whereas everything is less than infinity.

If we said that infinite groups had "order 0" (i.e. "order" meant "size if it's finite, and 0 if not"), and elements of infinite order also had order 0, then the standard theorems about order of the element/subgroup dividing the order of the group would be true even in the infinite case.

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