iiinova — where your digital self keeps evolving

Patrick Shafto @patrickshafto.bsky.social · 20/11/2025

Thrilled to be sponsoring the The 5th Workshop on Mathematical Reasoning and AI NeurIPS 2025! lnkd.in/dqXjrrcU lnkd.in/dzs3K3wZ

030

Reposted by Patrick Shafto

Kyle Cranmer @kylecranmer.bsky.social · 12/11/2025

It was a great honor and an inspiring conference. Thank you to the organizers and thank you to Margot and Tom Pritzker!

0132

Reposted by Patrick Shafto

Blake Bordelon @frostedblakess.bsky.social · 23/10/2025

Applying to do a postdoc or PhD in theoretical ML or neuroscience this year? Consider joining my group (starting next Fall) at UT Austin! POD Postdoc: oden.utexas.edu/programs-and... CSEM PhD: oden.utexas.edu/academics/pr...

13211

Reposted by Patrick Shafto

xenaproject.bsky.social @xenaproject.bsky.social · 09/10/2025

ItaLean : formal maths and AI in Italy (Bologna), Dec 2025. Lectures, hands-on tutorials, research talks from academia and industry etc. Register here pitmonticone.github.io/ItaLean2025/

pitmonticone.github.io

ItaLean 2025

083

Patrick Shafto @patrickshafto.bsky.social · 08/10/2025

Exciting opportunity for people at the intersection of math, AI, and formal methods! University of Michigan Math search: advanced assistant, or tenured associate or full professor for our initiative on Foundations of Artificial Intelligence mathjobs.org/jobs/list/26...

021

Patrick Shafto @patrickshafto.bsky.social · 15/09/2025

AI and math. Geometry and symbolic reasoning. Amazing recent developments and stellar line up of speakers. It is going to be an exciting week! The Geometry of Machine Learning @ Harvard Center for Mathematical Sciences and Applications (CMSA) cmsa.fas.harvard.edu/event/mlgeom...

060

Patrick Shafto @patrickshafto.bsky.social · 02/09/2025

Great to have this video about my @darpa.mil Artificial Intelligence Quantified (AIQ) program out! Very exciting program with absolutely fantastic teams. Stay tuned for some jaw dropping announcements! www.youtube.com/watch?v=KVRF...

youtube.com

AIQ: Artificial Intelligence Quantified

YouTube video by DARPAtv

071

Reposted by Patrick Shafto

Arno Solin @arnosolin.bsky.social · 12/08/2025

📣 Please share: We invite submissions to the 29th International Conference on Artificial Intelligence and Statistics (#AISTATS 2026) and welcome paper submissions at the intersection of AI, machine learning, statistics, and related areas. [1/3]

23721

Reposted by Patrick Shafto

Lean Focused Research Organization @lean-lang.org · 05/08/2025

We're excited to share the Lean FRO Year 3 Roadmap today! It builds on work completed in the first two years of Lean FRO operations and will guide all #LeanLang development through July 2026. ➡️ Read the roadmap at lean-lang.org/fro/ #LeanProver #FormalMathematics #FormalVerification

lean-lang.org

Lean Programming Language

Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code.

0115

Reposted by Patrick Shafto

xenaproject.bsky.social @xenaproject.bsky.social · 28/07/2025

I am advertising for 4 post-docs to come to Imperial and formalize, in Lean, *statements* of theorems from recent issues of the top generalist pure mathematics journals. www.imperial.ac.uk/jobs/search-... Positions are for 2 years, start date 1st Oct this year. Deadline 15th August.

imperial.ac.uk

Description

Please note that job descriptions are not exhaustive, and you may be asked to take on additional duties that align with the key responsibilities ment...

22913

Reposted by Patrick Shafto

xenaproject.bsky.social @xenaproject.bsky.social · 24/07/2025

A new "Mathlib initiative" focussed around Lean's mathematics library has been announced. Thanks to the generosity of Alex Gerko and XTX Markets, there is finally an official entity focussed on growing this 21st century way of doing mathematics. www.renaissancephilanthropy.org/news-and-ins...

renaissancephilanthropy.org

Lean FRO and Mathlib receive $10M from XTX Markets Founder Alex Gerko to further advance the use of AI for mathematical research — Renaissance Philanthropy – A brighter future for all through science,...

FOR IMMEDIATE RELEASE July 24, 2025 Contact: media@renphil.org ; richard.hillary@xtxmarkets.com ; pr@convergentresearch.org

0214

Reposted by Patrick Shafto

Terence Tao @teorth.bsky.social · 19/07/2025

My thoughts on the crucial importance of methodology on self-reported AI performance on mathematics competitions, and my policy on commenting on such reports going forward: mathstodon.xyz/@tao/1148814...

mathstodon.xyz

Terence Tao (@tao@mathstodon.xyz)

It is tempting to view the capability of current AI technology as a singular quantity: either a given task X is within the ability of current tools, or it is not. However, there is in fact a very wid...

223051

Reposted by Patrick Shafto

Alondra Nelson @alondra.bsky.social · 16/07/2025

New opportunity at the Institute for Advanced Study! The School of Social Science is hiring an Academic Assistant to support faculty & an international community of scholars. Pls share with folks in your network who might be interested in joining our team. recruiting.paylocity.com/recruiting/j...

recruiting.paylocity.com

Institute for Advanced Study - Academic Assistant - School of Social Science

Reporting to the School Administrative Officer, the incumbent will be responsible for providing broad administrative support to a faculty member and the School Administrative Officer.Position Duties a...

24038

Reposted by Patrick Shafto

RL & Agents Reading Group @rl-agents-rg.bsky.social · 10/07/2025

Hello world! This is the RL & Agents Reading Group We organise regular meetings to discuss recent papers in Reinforcement Learning (RL), Multi-Agent RL and related areas (open-ended learning, LLM agents, robotics, etc). Meetings take place online and are open to everyone 😊

13712

Reposted by Patrick Shafto

Terence Tao @teorth.bsky.social · 08/07/2025

The #SalemPrize for 2025 is now accepting nominations until September 15th. www.ias.edu/math/activit... (I am the chair of the Scientific Committee for the prize.) A bit more information in my blog post on this: terrytao.wordpress.com/2025/07/08/s...

Reposted by Patrick Shafto

Alondra Nelson @alondra.bsky.social · 28/06/2025

very interesting discussion. the contrast IK makes between mathematics and inductive neural networks is compelling. perhaps of interest @patrickshafto.bsky.social? thanks for digging it up and for your analysis, @natolambert.bsky.social .

141

Reposted by Patrick Shafto

Lean Focused Research Organization @lean-lang.org · 23/06/2025

In this 10-minute UCLA Connect talk, Terence Tao provides an accessible and compelling argument for "citizen math" and broad collaboration in research #mathematics via #formalverification using proof assistants like #LeanLang. 🎥 www.youtube.com/watch?v=K376...

0105

Reposted by Patrick Shafto

Alondra Nelson @alondra.bsky.social · 20/06/2025

ICYMI RARE/EARTH: The Geopolitics of Critical Minerals + the AI Supply Chain w/ @triofrancos.bsky.social @katecrawford.bsky.social @tamigraph.bsky.social @hofrench.bsky.social www.youtube.com/watch?v=GxVM... Opening remarks albert.ias.edu/server/api/c... Event brief www.ias.edu/stsv-lab/aig...

Poster reading Rare/Earth The geopolitics of critical minerals and the AI supply chain, with pictures of Thea Riofrancos, Providence College
Tamara Kneese, Data and Society
Howard French, Columbia University (Only attending Public Panel)
Kate Crawford, University of Southern California and Microsoft Research
Alondra Nelson, Institute for advanced study

06223

Reposted by Patrick Shafto

Lean Focused Research Organization @lean-lang.org · 19/06/2025

Congrats! We're excited to see what projects come from expMath!

021

Patrick Shafto @patrickshafto.bsky.social · 19/06/2025

NY times article on expMath, my AI for math @darpa.mil program, with commentary from mathematicians Andrew Granville, Bryna Kra, Jordan Ellenberg, and context from IAS professor @alondra.bsky.social ocial and @anthropic.com CEO @darioamodei.bsky.social www.nytimes.com/2025/06/19/s...

nytimes.com

Can A.I. Quicken the Pace of Math Discovery?

180

Reposted by Patrick Shafto

Amstat-American Statistical Association @amstatnews.bsky.social · 17/06/2025

In his latest "Amstat News" piece, David Corliss spotlights the JEDI programming at the upcoming Joint Statistical Meetings in Nashville (Aug 2–7). Don't miss this essential guide to making the most of JEDI at JSM. magazine.amstat.org/blog/2025/06...

021

Reposted by Patrick Shafto

American Mathematical Society @amermathsoc.bsky.social · 12/06/2025

See Playing with Shape and Form: A Glimpse of Topology in action! Check out a clip of a classroom using the book, which is up to 35% off during the AMS Summer Reading Sale — ends July 4. Watch here: www.youtube.com/watch?v=tjrN... Shop here: bookstore.ams.org/view?Product... #MathSky

Playing with Shape and Form: A Glimpse of Topology book cover.

021

Reposted by Patrick Shafto

eleutherai.bsky.social @eleutherai.bsky.social · 06/06/2025

Can you train a performant language model using only openly licensed text? We are thrilled to announce the Common Pile v0.1, an 8TB dataset of openly licensed and public domain text. We train 7B models for 1T and 2T tokens and match the performance similar models like LLaMA 1 & 2

214660

Patrick Shafto @patrickshafto.bsky.social · 04/06/2025

Excited to have my @darpa.mil program on AI for pure math, Exponentiating Mathematics, featured in @technologyreview.com! #expMath

020

Patrick Shafto @patrickshafto.bsky.social · 04/06/2025

Excited to have my @darpa.mil program on AI for pure math, Exponentiating Mathematics, featured in @technologyreview.com! #expMath

010

Reposted by Patrick Shafto

Simons Institute for the Theory of Computing @simonsinstitute.bsky.social · 23/05/2025

“The intuition is just so simple,” Williams said. “You can reuse space, but you can’t reuse time.” Read @benbenbrubaker.bsky.social's piece for @quantamagazine.bsky.social on @rrwilliams.bsky.social's landmark result sharpening our understanding of time-space tradeoffs.

quantamagazine.org

For Algorithms, a Little Memory Outweighs a Lot of Time | Quanta Magazine

One computer scientist’s “stunning” proof is the first progress in 50 years on one of the most famous questions in computer science.

0214

Reposted by Patrick Shafto

Gabriel Peyré @gabrielpeyre.bsky.social · 20/05/2025

I have updated my slides on the maths of AI by an optimal pairing between AI and maths researchers ... speakerdeck.com/gpeyre/the-m...

3253

Reposted by Patrick Shafto

Lean Focused Research Organization @lean-lang.org · 14/05/2025

This is a great experiment in autoformalization using cutting-edge tools (Canonical: github.com/chasenorman/...) within an actively developed research project (Equational Theories: teorth.github.io/equational_t...) Thanks for sharing @teorth.bsky.social! #LeanLang #LeanProver

teorth.github.io

Equational Theories Project

Mapping out the relations between different equational theories of Magmas

051

Reposted by Patrick Shafto

Alondra Nelson @alondra.bsky.social · 14/05/2025

Register to join this timely discussion on June 2, in person or on line, with @katecrawford.bsky.social @hofrench.bsky.social @tamigraph.bsky.social and @triofrancos.bsky.social, hosted by my Science, Technology, and Social Values Lab at the Institute for Advanced Study www.ias.edu/events/raree...

614379

Reposted by Patrick Shafto

Terence Tao @teorth.bsky.social · 11/05/2025

As an experiment, I tried to use automated tools to formalize (in as "mindless" a fashion as possible) a one-page human written proof into Lean. You can watch the results here: www.youtube.com/watch?v=cyyR...

youtube.com

Formalizing a proof in Lean using Github copilot and canonical

YouTube video by Terence Tao

210611

Reposted by Patrick Shafto

Timothy Gowers @wtgowers.bsky.social · 11/05/2025

Wow, looking forward to this!

1121

Patrick Shafto @patrickshafto.bsky.social · 06/05/2025

Spent last week @ias with DeepMind math teams. AlphaProof, AlphaGeometry, PDEs, and PAIRs teams were there with leadership. Impressed by the collaboration. Huge, open technical problems to be solved. Exciting times for mathematics & AI! www.ias.edu/math/events/...

180

Reposted by Patrick Shafto

David Pfau @davidpfau.com · 02/05/2025

New paper accepted to ICML! We present a novel policy optimization algorithm for continuous control with a simple closed form which generalizes DDPG, SAC etc. to generic stochastic policies: Wasserstein Policy Optimization (WPO).

29410

Reposted by Patrick Shafto

Terence Tao @teorth.bsky.social · 01/05/2025

DARPA's "Exponentiating mathematics" (expMath) program, which is launching a challenge to develop and evaluate "AI collaborators" for assist in decomposing and formalizing informal mathematical proofs, is now taking short abstract proposal submissions: sam.gov/opp/869c8d73...

sam.gov

SAM.gov

5256

Patrick Shafto @patrickshafto.bsky.social · 30/04/2025

The Exponentiating Mathematics (expMath) program BAA has dropped! sam.gov/opp/869c8d73... Abstracts due May 15. Be sure to register on the submission website well in advance! (A few days ahead!)

020

Patrick Shafto @patrickshafto.bsky.social · 27/04/2025

Great talks at the "Autoformalization for the Working Mathematician" workshop at Institute for Computational and Experimental Research in Mathematics @icerm.bsky.social yesterday. Today was another great lineup. Very much worth checking out the videos! icerm.brown.edu/program/hot_...

icerm.brown.edu

060

Reposted by Patrick Shafto

Jesse Farebrother @brosa.ca · 22/04/2025

Excited to be in Singapore 🇸🇬 for #ICLR25! We’ll present 1) Meta Motivo, a first-of-its-kind model enabling zero-shot humanoid control for any reward, goal, or motion; 2) imitation via successor feature matching; 3) flow matching for generative TD learning of future experience.

191

Reposted by Patrick Shafto

Simons Institute for the Theory of Computing @simonsinstitute.bsky.social · 16/04/2025

The room is full for @yoshuabengio.bsky.social's Richard M. Karp Distinguished Lecture on "Superintelligent Agents Pose Catastrophic Risks — Can Scientist AI Offer a Safer Path?" at the Simons Institute. Umesh Vazirani getting ready to introduce Yoshua Bengio. simons.berkeley.edu/events/super...

071

Reposted by Patrick Shafto

Lénaïc Chizat @lenaicchizat.bsky.social · 14/04/2025

Announcing : The 2nd International Summer School on Mathematical Aspects of Data Science mathsdata2025.github.io EPFL, Sept 1–5, 2025 Speakers: Bach @bachfrancis.bsky.social Bandeira Mallat Montanari Peyré @gabrielpeyre.bsky.social For PhD students & early-career researchers Apply before May 15!

mathsdata2025.github.io

Mathematical Aspects of Data Science

Graduate Summer School - EPFL - Sept. 1-5, 2025

14424

Patrick Shafto @patrickshafto.bsky.social · 07/04/2025

Excited for the kickoff of "AI for Mathematics and Theoretical Computer Science" @simonsinstitute.bsky.social today! simons.berkeley.edu/workshops/si...

simons.berkeley.edu

Schedule

191

Reposted by Patrick Shafto

José A. Alonso @jalonso.eurosky.social · 28/03/2025

Verified collaboration: How Lean is transforming mathematics, programming, and AI. ~ Leonardo de Moura. youtu.be/rmMYFmlUbJ8 #ITP #LeanProver #Math #Programming #AI

youtu.be

Leonardo de Moura - Verified Collaboration: How Lean is Transforming Math...(March 12, 2025)

YouTube video by Simons Foundation

182

Patrick Shafto @patrickshafto.bsky.social · 26/03/2025

Proposer's day for expMath has dropped! Accelerate progress in pure math via AI capable of proposing and proving useful abstractions Teams either: - develop AI capable of auto decomposition and auto(in)formalization - evaluate with respect to professional math

160

Patrick Shafto @patrickshafto.bsky.social · 26/03/2025

Mathjobs has been down for a week...which is kinda an issue. Many people on both sides are in limbo. :-/

020

Reposted by Patrick Shafto

Simons Institute for the Theory of Computing @simonsinstitute.bsky.social · 05/03/2025

Hello, World! Looking forward to connecting with you about new research in CS theory and what's happening in the Simons Institute's research programs, workshops, pods, and public lectures.

2586

Reposted by Patrick Shafto

Lean Focused Research Organization @lean-lang.org · 03/03/2025

We're building a more responsive #LeanLang experience! UI upgrades include better performance, auto-completion and clearer error messages. Backend enhancements bring parallelism for faster builds, reduced latency, and soon a new module system for quicker recompilation times. #leanprover #programming

0144

Reposted by Patrick Shafto

Clément Canonne @ccanonne.github.io · 28/02/2025

The Simons Institute is now on BlueSky! 🍾 Follow them: @simonsinstitute.bsky.social #TCSSky

26416

Reposted by Patrick Shafto

Ryan Williams @rrwilliams.bsky.social · 21/02/2025

New paper: Simulating Time With Square-Root Space people.csail.mit.edu/rrw/time-vs-... It's still hard for me to believe it myself, but I seem to have shown that TIME[t] is contained in SPACE[sqrt{t log t}]. To appear in STOC. Comments are very welcome!

people.csail.mit.edu

1726475

Reposted by Patrick Shafto

Lean Focused Research Organization @lean-lang.org · 27/02/2025

Mathlib is a community-built library of mathematics in Lean with nearly 1.8MM lines of code and 190K mathematical theorems! Over 500 contributors have helped drive Mathlib forward at an incredible pace! Learn more at: leanprover-community.github.io/index.html #leanlang #leanprover #community

085