On today's episode of @scifri.bsky.social, @littmath.bsky.social
and I had a conversation about vibe proving and AI for mathematics.
Check it out here:
www.sciencefriday.com/segments/cou...
🚨 Putting this back on your radar:
The deadline for the ICERM Graduate Training Workshop on ∞-categories with proof-assistants (organized with @emilyriehl.bsky.social and Jonathan Weinberger) is getting close!
📬Application deadline: March 31, 2026.
Full details + links in the post below 👇
If these challenges interest you and you are planning to attend the Joint Mathematics Meetings, join us tomorrow, Monday, and Tuesday for a great cluster of activities around the theme of Communicating Mathematics, organized by Katie Mann and others:
sites.google.com/view/communi...
This conversation was a follow-up to a column I wrote on the same topic entitled "Mathematics is hard for mathematicians to understand too"
www.science.org/doi/10.1126/...
On the latest episode of the Science podcast, Alex Kontorovich and I discuss the challenges of communicating mathematics among professional mathematicians:
www.science.org/content/podc...
After the semester ended, I reordered several of the worlds and made various edits and additions. Further contributions are very welcome, especially in the form of PRs to:
github.com/emilyriehl/R...
In particular, Jon Eugster saved me several times, when I needed help (or back end fixes) in a rush before my text class.
This game was made possible by the good folks who built the Lean Game Skeleton repository and answered questions on the Lean for teaching thread on the Lean zulipchat, such as Alex Kontorovich, Aaron Liu, and Dan Velleman.
The prefix "re" the title imagines more experienced players who might like to learn more about dependent type theory, the Curry Howard correspondence, or constructive mathematics.
Following a suggestion made by Kevin Buzzard this past summer, there is a world studying constructions involving the empty type before introducing negations, which allows us to separate out constructive proofs (eg double negation introduction) from classical ones (like double negation elimination).
The game uses Lean tactics to animate the analogy between function types and implications, product types and conjunctions and so on.
This past fall, I taught a first year seminar course at Johns Hopkins along these lines. As part of the course, I developed the Reintroduction to Proofs Game:
adam.math.hhu.de#/g/emilyrieh...
which is now featured on the Lean Game Server:
adam.math.hhu.de
In a talk called "A reintroduction to proofs"
emilyriehl.github.io/files/reintr...
I've speculated about teaching an undergraduate level introduction to proofs course but using dependent type theory as the implicit formal system in place of set theory and first order logic.
Glad you liked it!
very fabulous and provocative talk for a non-specialist audience about developing new mathematics, vibe proving and mathematical rigor between human mathematicians and computational mathematics in the age of AI by @emilyriehl.bsky.social, among other things-- highly recommend
I don't unfortunately but if you ever come across something please let me know.
One of my favorites from Bill Thurston ❤️:
Anyone registered for the conference is welcome to participate. More info about the Joint Meetings can be found here:
jointmathematicsmeetings.org/jmm
Here is a website describing activities around the challenge of communicating mathematics to be at the upcoming Joint Mathematics Meetings from January 4-7, 2026:
sites.google.com/view/communi...
I wrote about the challenge of mathematicians explaining mathematics to other mathematicians for
Science Magazine's Expert Voices column series:
www.science.org/doi/10.1126/...
@sciam.bsky.social gave me the opportunity to share some personal thoughts about the recently reported AI results from the #imo2025:
www.scientificamerican.com/article/math...
In June, Tao gave an online talk on the twin primes conjecture as part of Scientific Webinars in Solidarity with Palestine. “Sometimes you wonder what’s the point of doing mathematics in such a time,” he said to the virtual audience. “But at least one thing that mathematics offers is that it’s at least one place where we can actually resolve even very bitter disputes.”
While reporting, I stumbled across a recent talk that Tao gave on the subject of his latest research. youtu.be/cXqz5hgxlLM
The suspensions landed perhaps most heavily in math. NSF suspended a $25 million grant for the Institute for Pure and Applied Mathematics (IPAM), an international center at UCLA that hosts about 2000 visiting researchers every year for workshops and other programs. One of its stars, Terence Tao, a Fields Medal winner frequently named as one of the greatest living mathematicians, also had his only NSF grant suspended. The $750,000 award was in its first year and supported Tao’s own research and a handful of graduate students in developing tools to tell whether a set of numbers is structured or random. Tao says he now cannot offer research assistant opportunities during the academic year, and he calls the cuts to IPAM “quite disastrous.” Tao’s ultimate goal is to use the tools to solve the twin primes conjecture, a centuries-old problem in number theory that suggests there are an infinite number of prime pairs that differ by two, like five and seven. But the NSF grant provided the vast majority of outside support for his UCLA salary. “I’m currently doing summer research unfunded,” he says.
Math at UCLA suffered the greatest blow.
I spoke with Terry Tao—Fields Medalist and arguably the preeminent mathematician of his generation—who is apparently now doing his summer research in number theory without external funding.
The Trump administration is launching a new wave of attacks on universities, and UCLA is the latest target.
My reporting on how the university has been hit and how some of its scientists are responding:
www.science.org/content/arti...
One thing I've always appreciated about the NSF is their broad mission to "promote the progress of science" both through new research and its public communication. See the following thread for #DMSFunded work describing recent developments in category theory, homotopy theory, and formalization:
In particular, I'll be highlighting three essays by
@federicoardila.bsky.social, Denis R. Hirschfeldt, and @ijlaba.bsky.social linked from the last page of the slides.
This talk revisits a conversation held at Johns Hopkins in 2019 the proceedings of which were published by the
@amermathsoc.bsky.social
bookstore.ams.org/mbk-140
the mathematical landscape. We will raise questions related to building communities in which all mathematicians can flourish, rewarding collective work, organizing labor, confronting climate change, and anticipating AI.''
Norms are local — they are how individuals interact with each other and how individuals act in an institution — and global — our work at the local level building community glues to the work of our colleagues at other institutions, creating a systemic awareness and change across
