Notes on AI for Math­e­mat­ics and The­o­ret­i­cal Com­put­er Sci­ence

In April 2025 I had the plea­sure to at­tend an in­tense week-long work­shop at the Si­mons In­sti­tute for the The­o­ry of Com­put­ing en­ti­tled AI for Math­e­mat­ics and The­o­ret­i­cal Com­put­er Sci­ence. The event was or­ga­nized joint­ly with the Si­mons Laufer Math­e­mat­i­cal Sci­ences In­sti­tute (SLMath, for short). It was an in­tense time (five ful­ly-packed days!) for learn­ing a lot about cut­ting-edge ideas in this in­ter­sec­tion of for­mal math­e­mat­ics (pri­mar­i­ly in Lean), AI, and pow­er­ful tech­niques for solv­ing math­e­mat­i­cal prob­lems, such as SAT solvers and de­ci­sion pro­ce­dures (e.g., the Wal­nut sys­tem). Videos of the talks (but not of the train­ing ses­sions) have been made avail­able.

Every day, sev­er­al dozen peo­ple were in at­ten­dance. Judg­ing from the ar­ray of un­claimed badges (eas­i­ly an­oth­er sev­er­al dozen), quite a lot more had signed up for the event, but didn't come for one rea­son or an­oth­er. It was in­spir­ing to be in the room with so many peo­ple in­volved in these ideas. The train­ing ses­sions in the af­ter­noon had a great vibe, since so many peo­ple we learn­ing and work­ing to­geth­er si­mul­ta­ne­ous­ly.

It was great to con­nect with a num­ber of peo­ple, of all stripes. Most of the pre­sen­ters and at­ten­dees were com­ing from acad­e­mia, with a mi­nor­i­ty, such as my­self, com­ing from in­dus­try.

The or­ga­ni­za­tion was fan­tas­tic. We had talks in the morn­ing and train­ing in the af­ter­noon. The fi­nal talk in the morn­ing, be­fore lunch, was an in­tro­duc­tion to the af­ter­noon train­ing. The train­ing top­ics were:

Day 1

Lean with María Inés de Fru­tos-Fer­nán­dez

Day 2

Ma­chine learn­ing with Sean Welleck

Day 3

SAT solv­ing (more ex­am­ples) with Mar­i­jn Heule

Day 4

Tools & demos, and/or con­tin­ue ear­li­er train­ing

Day 5

Open dis­cus­sion

The links above point to the tu­to­r­i­al git re­pos for fol­low­ing along at home.

In the open dis­cus­sion on the fi­nal af­ter­noon, I raised my hand and out­ed my­self as some­one com­ing to the work­shop from an in­dus­try per­spec­tive. Al­though I had al­ready met a few peo­ple in in­dus­try pri­or to Fri­day, I was able to meet even more by rais­ing my hand and invit­ing fel­low prac­tion­ers to dis­cuss things. This led to meet­ing a few more peo­ple.

The talks were fas­ci­nat­ing; the se­lec­tion of speak­ers and top­ics was ex­cel­lent. Go ahead and take a look at the list of videos, pick out one or two of in­ter­est, grab a bev­er­age of your choice, and en­joy.