Seewoo Lee retweeted
On Oct 6, OpenAI released 719 AI-generated math manuscripts. To help the community digest them, we built oai-math-revised: browse the papers by category, follow revisions and retractions, and add citations, follow-up work and corrections.
mathcommunity.github.io/oai-…
Seewoo Lee retweeted
New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: anthropic.com/research/forma…
Seewoo Lee retweeted
Wouter van Doorn and I have written a short paper explaining the 'Egyptian fraction' paper included in the recent OpenAI proofs.
Not the most important of the recent proofs, but this is a favourite topic of ours (and of Erdős).
erdosproblems.com/static/Uni…
Some comments:
1/
I just gave a talk on this: seewoo5.github.io/teaching/a…
Seewoo Lee retweeted
Apart from general awkwardness, mathematicians are at a disadvantage in discourse because the general public (including much of the twitterati) has very little sense of what we do. I like the activity of solving problems/proving theorems but math research is not a problem set.
Seewoo Lee retweeted
Interesting reading Frank Calegari's opinion on the new @OpenAI results!
He is actually one of my favorite math writers. Always witty and insightful.
galoisrepresentations.org/20…
Seewoo Lee retweeted
(auto)formalization, but why proofsandprompts.com/2026/09…
Seewoo Lee retweeted
We've updated our GitHub math repo with 6 new Lean formalizations, 19 modifications, and 3 withdrawals. The repo now has ~42% top-line results formalized. We will continue to update the repo with new formalizations and with any errata we notice.
github.com/openai/math/blob/…
Seewoo Lee retweeted
Jineon Baek is one of the best mathematicians you never heard of. In 2024 he astonished the world with his solution of the moving sofa problem. I created this video to celebrate his achievement and 60 years of moving sofas. Pro tip: watch with the sound on (it's SFW). 1/4
Seewoo Lee retweeted
Thoughts on math and AI. Are human mathematicians redundant in a world in which AIs are better than humans at proving theorems? The answer may surprise you.
blog.danromik.com/the-feedba…
Seewoo Lee retweeted
Hello, world! There is a new repository for works in math and TCS: hexagonmath.org, now in public beta. Please try it out and submit something! We welcome your feedback while we build and improve it.
youtu.be/yOBTwerVIq8?is=g3n2… I truely enjoyed this talk last week
Seewoo Lee retweeted
I was part of a group that met last week to try to propose recommended changes to the structure of math PhD programs in an age of AI. Our report, together with a collection of related resources, is now available here:
cmsa.fas.harvard.edu/aimathp…
Seewoo Lee retweeted
A faculty friend of mine once gave me this (amazing) classification of motivations present in professional mathematicians for doing mathematics: 1. Science (understanding of phenomena) 2. Art (beauty, style) 3. Systematization (what is the “right language”) 4: Sport (prizes).
Different mathematicians have different mixes, all are quite present in aggregate. These different motivations explain many of the different reactions to the AI advances!
Seewoo Lee retweeted
There has been a recent surge of fantastic essays about mathematics and AI, representing a range of viewpoints.
I recommend reading them all.
If, like me, you prefer a PDF I am collecting these at thomasbloom.org/AIEssays.pdf
(Currently 16 articles and 55 pages.)
I don't know if anyone still cares but I do, so: I digested the Astra's proof on the sphere packing problem (more precisely, Cohn-Elkies bound and Bourgain-Clozel-Kahane sign uncertainty principle). I wrote two blog posts:
I decided to refactor the formalization and it ended up with the following: github.com/seewoo5/cohn-elki… The single-file version is about half of the original formalization in terms of LoC (which is not the ideal metric though), where it also proves some missing results
