← Feed

Posts

• View post

  Big news on irrational numbers! Aabir Fauzan from Aalto University released a preprint on Zenodo before it hit the arXiv, and a formalisation has been posted by Moritz Firsching. Since the statement is so elementary, the repo is set up to be checked by the stringent anti goal-hacking framework Comparator, and moreover the machinery used is the PNT+ project run by @tao@mathstodon.xyz and Alex Kantorovic, which is high-quality hand-rolled analytic number theory in Lean, I'm fairly confident t...

• View post

  "The situation isn’t quite like the situation in chess, where powerful chess programs got to the point they could beat humans, but human to human chess competition survived. Where we’re going could be analogous to chess playing where everyone is using, with or without acknowledging it, some sort of chess program." — @peterwoit@mathstodon.xyz (https://www.math.columbia.edu/~woit/wordpress/?p=15787) I'm kinda sick of people comparing the use of AI in math to the use of engines che...

• View post

  From @DavidKButler@mathstodon.xyz https://davidkbutler.xyz/2026/06/25/two-sided-ruler-constructions-1-introduction/ a sequence of blog posts, with accompanying videos and a detailed index of geometric constructions in this constrained setting. Going to be a fun read!

• View post

  This is a big deal. Also, Joan Birman is 99 years old and still going! https://arxiv.org/abs/2607.05283

• View post

  From @johncarlosbaez "I think it's better to figure out the theorems before stating the definitions. That is: figure out the patterns that hold, and turn these into theorems (or at least conjectures), and then notice that these theorems are easiest to state if one makes certain definitions." https://categorytheory.zulipchat.com/#narrow/channel/229156-theory.3A-applied-category-theory/topic/Networks.20in.20Biology/near/531125772

• View post

  Where are the Fields medallists who work outside the topics that @wtgowers and @tao 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...

• View post

  I'm really glad to see that the Journal of Lie Theory is now diamond open access! https://jolt.centre-mersenne.org/

• View post

  "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.

• View post

  Statement from the @AustMS 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...

• View post

  RE: https://mathstodon.xyz/@nbourbaki/116170301181239832 That Scholze lecture .... 👀

• View post

  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 Buzzard is deliberately *not* formalising i...

• View post

  https://mathoverflow.net/q/510716/4177 an abstract question with a concrete motivating example

• View post

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

• View post

  RE: https://mastoxiv.page/@arXiv_mathCT_bot/116452870261810513 This is fun

• View post

  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.

• View post

  English translation and refresh of a 1957 classic article that treats non-Hausdorff manifolds. A bunch of nice 1-dimensional examples are discussed near the beginning, with pictures https://arxiv.org/abs/2208.11193

• View post

  I found out from Mochizuki's recent talk about AI/formalisation for mathematics, that someone managed to recently convince him about something Zoran Skoda and I knew and understood about the set-theoretic material in IUT4 in late 2012, specifically about what he called 'species' and 'mutations'. But also, the next step is to fully convince him that POV is wholly unnecessary. He mentioned this as well, in light of him looking to use Lean to formalise parts...

• View post

  RE: https://mathstodon.xyz/@MartinEscardo/116444953374441218 "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."

• View post

  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 thousand...

• View post

  I have a hankering to completely rewrite Makkai's anafunctor paper as internal categories in a well-pointed class category, rather than how it's currently specified, which is essentially using some kind of dependent types machinery.

• View post

  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)

• View post

  RE: https://mathstodon.xyz/@slava/116377939182668511 Nice. "Prior to this paper, all small simple groups were known to be efficient, but the status of four of their covering groups was unknown. Nice, efficient presentations are provided in this paper for all of these groups, resolving the previously unknown cases. The authors‘ presentations are better than those that were previously available, in terms of both length and computational properties. In many cases, these presentations hav...

• View post

  RE: https://mathstodon.xyz/@dougmerritt/116166624131816531 Very interesting essay by de Moura.

• View post

  RE: https://mathstodon.xyz/@varkor/116217000387640077 #icanhazpdf https://doi.org/10.18311/jims/1960/16908

• View post

  For all the excitement about Math Inc.'s AI tool Gauss proving Erdős problem #1196 (4 typeset pages), and then it being formalised in Lean in 7000-ish ('golfed', i.e. reduced, to 4000-ish) lines of code, @tao [1] has mathematician-golfed the proof to two paragraphs using standard analytic number theory tools, with one very easy helper lemma about weighted graphs. It suppresses some details about how some estimates are achieved, but it reads like something Tao would blog a...

• View post

  RE: https://mathstodon.xyz/@antoinechambertloir/116431983042529927 💯 💯 💯 💯 💯 💯 💯

• View post

  From @xenaproject 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 L...

• View post

  Just because @xenaproject has banged on about it so much, I caught this moment of saying "canonical isomorphism" and writing an equals symbol.... ;-P Points out that he didn't write \(\cong\), and that "maybe I'll say that "=" means "canonically isomorphic to" in this context."

• View post

  > Osmanovic Thunström planted many clues in the preprints to alert readers that the work was fake. Izgubljenovic works at a non-existent university called Asteria Horizon University in the equally fake Nova City, California. One paper’s acknowledgements thank “Professor Maria Bohm at The Starfleet Academy for her kindness and generosity in contributing with her knowledge and her lab onboard the USS Enterprise”. Both papers say they were funded by “the Professor Sideshow Bob Foundation for...

• View post

  New from @DavidKButler https://davidkbutler.xyz/2026/03/24/three-types-of-infinity/ David includes a disclaimer to ward off people complaining, but I see nothing to complain about. Here's some thoughts it gave me. The use of ∞ to refer to the location at the (positive) end of the number line is a very nice way to put it. If you think of convergent sequences in say metric spaces, the "infinity" point of a sequence is its limit. And the "abstract convergent se...