theHigherGeometer

Where are the Fields medallists who work outside the topics that @wtgowers@mathstodon.xyz and @tao@mathstodon.xyz work on, and who are seeing LLMs solve actual problems in their areas of expertise? (Viazovska's work being autoformalised doesn't count, it was not somewhat autonomously being improved by AI, being pushed in new directions)

https://chadtopaz.com/essays/gowers-response

Are they just not being courted by AI companies? Or seeing no good results? We really need to hear analysis of negative results as well. I've read Scholze is not a fan, on principle.

Statement from the @AustMS@mathstodon.xyz about #ICM2026

"To the International Mathematics Union,

The Australian Mathematical Society calls upon the IMU to reconsider Philadelphia in the USA as host venue for the 2026 ICM due to potential difficulties for international delegates to obtain visas to attend, the potential risks to international delegates arising from the activities of the USA’s Immigration and Customs Enforcement officers, and the potential dangers arising from the involvement of the host nation in current warfare.

Yours sincerely,
Aidan Sims
President of the Australian Mathematical Society
(May 1, 2026)"

source: https://sites.google.com/view/icm2026boycott/societies

h/t @Rowena@mathstodon.xyz

RE: @MartinEscardo@mathstodon.xyz

"The proofs are therefore sound, but the definitions are less reusable than they could be—a user inheriting these definitions without the accompanying assumptions could derive spurious results. This pattern is characteristic of LLM-generated code: the model reliably produces definitions that are sufficient for the proofs at hand but does not anticipate downstream reuse or defensive design."

I'm really glad to see that the Journal of Lie Theory is now diamond open access!

https://jolt.centre-mersenne.org/

A rumour has reached your correspondent's ears that a group led by S.-T. Yau is working on formalising the Classification of Finite Simple Groups. No public announcement to confirm, a specific university was mentioned where people got emails about it.

The scale of such a project is beyond anything anyone has attempted before, as the proof is thousands of pages, not fully written out cleanly in a "self-contained" way yet by the GLS(+others) team, and depends on thousands of pages of "background" material as assumed knowledge, itself not fully isolated out of reference works.

https://www.quantamagazine.org/a-powerful-new-qr-code-untangles-maths-knottiest-knots-20260422/ with (very fun!) paper https://arxiv.org/abs/2509.18456

"The 21st century produces workers who tell themselves there is nothing they cannot achieve. Han argues this is not liberation, but a sophisticated form of oppression. The whip is now held by the self."

https://www.abc.net.au/news/2026-05-10/burnout-symptoms-depression-anxiety-job-work-who-is-responsible/106658950

I do worry about university colleagues burning out.

Scanned notes from old lectures by Lawvere (some j.w.w. Joyal), taken by Anders Kock and shared in the last few years:

https://github.com/conceptualmathematics/Naturality

The dates are from 1966, 1971 (one lecture each), 1978 (five lectures), 2011 (one lecture)

Hunting down a living relative (who isn't a public figure) of a deceased academic on the internet feels a little stalkery, but it's for historical research, there's no alternative but to find people and talk to them.

I'd like to know which parts of this

https://upcommons.upc.edu/server/api/core/bitstreams/905201be-de7e-4a3c-8880-066122168679/content

are really finitary and elementary, and which step or steps are the really hard parts. This is a survey of the proof of Mazur's theorem that the p-torsion elements (for p a prime) in E(Q), for a rational elliptic curve E, must have p ≤ 13. This is a *big* hard component for FLT that Kevin @xenaproject@mathstodon.xyz Buzzard is deliberately *not* formalising in Lean. I'm listening to a recent talk by Colin McLarty (https://www.youtube.com/watch?v=sEduqKTK4ko) about FLT and the very slow-burning idea that one might be able to prove that it's provable in PA in the technical sense.

To my inexpert eyes, Lemma 2.2 in the linked pdf looks like something that could conceiably be reduced to a finitary argument (the only hard part seems to be talking about E[p] as a representation of the absolute Galois group of Q, but that presumably can be reduced to the system of representations of Galois groups of number fields). The other half that, to my understanding, goes to prove the main theorem is Lemma 2.3 and that is immediately serious, with Néron models etc.

I know this is ε progress on both big projects, but I think actually isolating the hard kernel theorems is psychologically helpful. I know Kevin is working "mod-1980s", but having a "boss level" (in his terms) that is Lemma 2.3 here (a certain finite extension of the p-th cyclotomic field is unramified) feels more satisfying to me than the monolithic th;df "Mazur's Theorem" (=too hard; didn't formalise).

RE: @antoinechambertloir@mathstodon.xyz

💯 💯 💯 💯 💯 💯 💯

RE: @arXiv_mathCT_bot@mastoxiv.page

This is fun

From @xenaproject@mathstodon.xyz https://tinyurl.com/JacobianChallenge a challenge to AI companies to autoformalise a nontrivial piece of well-known 19th century mathematics that will need new definitions etc that aren't in mathlib. Can an AI system adequately build the foundational material and 'API' for it that can then be used to give serious results? Unlike eg the sphere-packing formalisation by Math Inc that used a large amount of work by people that set up all the scaffolding in Lean (not to mention the rich Blueprint document that stated all the needed results for at least the 8-dim case)

https://mathoverflow.net/q/510716/4177

an abstract question with a concrete motivating example