Loading...
Organizing Committee
Northwestern University
Case Western Reserve University
Wayne State University
University of Washington
UCLA
Abstract
Spheres are the basic building blocks of geometry. More complicated geometric objects can be built by attaching spheres to each other along continuous maps. For many purposes, such constructions depend only on the homotopy classes of these continuous maps. A fundamental problem in algebraic topology is to compute these homotopy classes, i.e., to compute the homotopy groups of spheres. Machines can be used to great effect in the exhaustive computation of these fundamental invariants of homotopy theory.
The workshop will study several software packages that are specifically designed for this purpose. Participants will have the opportunity to interact directly with codebases in work groups led by experienced programmers. The workshop will also introduce a variety of projects in homotopy theory that rely on computers.
This program will foster the community of researchers who are working with machines to solve long-standing problems in homotopy theory. It will also connect that community with researchers who are using machines in related fields, such as applied topology, category theory, commutative algebra, and number theory.
Application Deadline March 13, 2026
The workshop will study several software packages that are specifically designed for this purpose. Participants will have the opportunity to interact directly with codebases in work groups led by experienced programmers. The workshop will also introduce a variety of projects in homotopy theory that rely on computers.
This program will foster the community of researchers who are working with machines to solve long-standing problems in homotopy theory. It will also connect that community with researchers who are using machines in related fields, such as applied topology, category theory, commutative algebra, and number theory.
Application Deadline March 13, 2026
Loading...
Loading participant list in background...
Workshop Schedule
Monday, June 22, 2026
8:30 - 8:50 AM EDT
Check In
11th Floor Collaborative Space
8:50 - 9:00 AM EDT
Welcome
11th Floor Lecture Hall
9:00 - 9:15 AM EDT
Group Project 1 Presentation
11th Floor Lecture Hall
Speaker
John Palmieri, University of Washington
Session Chair
Dan Isaksen, Wayne State University
9:15 - 9:30 AM EDT
Group Project 2 Presentation
11th Floor Lecture Hall
Speaker
Robert Chatham, Cloudflare
Session Chair
Dan Isaksen, Wayne State University
9:30 - 9:45 AM EDT
Group Project 3 &4 Presentation
11th Floor Lecture Hall
Speaker
Thomas Brazelton, Harvard University
Speaker
Ben Spitz, Indiana University Bloomington
Session Chair
Dan Isaksen, Wayne State University
9:45 - 10:00 AM EDT
Group Project 5 Presentation
11th Floor Lecture Hall
Speaker
Achim Krause, University of Oslo
Session Chair
Dan Isaksen, Wayne State University
10:00 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 10:45 AM EDT
Group Project 6 Presentation
11th Floor Lecture Hall
Speaker
Danny Shi, University of Washington
Session Chair
Dan Isaksen, Wayne State University
10:45 - 11:00 AM EDT
Group Project 7 Presentation
11th Floor Lecture Hall
Speaker
Eva Belmont, Case Western Reserve University
Session Chair
Dan Isaksen, Wayne State University
11:00 AM - 12:00 PM EDT
Group Discussion About Projects
Program Overview - 11th Floor Lecture Hall
12:00 - 1:30 PM EDT
Lunch/Free Time
1:30 - 3:00 PM EDT
Group Work / Software Installation
Group Work - Assigned Locations
3:00 - 3:30 PM EDT
Coffee Break
11th Floor Collaborative Space
3:30 - 5:00 PM EDT
Group Work
Assigned Locations
5:00 - 6:30 PM EDT
Reception
11th Floor Collaborative Space
Tuesday, June 23, 2026
9:30 - 10:00 AM EDT
TBA
11th Floor Lecture Hall
Speaker
Thomas Brazelton, Harvard University
Session Chair
Danny Shi, University of Washington
10:15 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:00 AM EDT
Topology and algebra in SageMath
11th Floor Lecture Hall
Speaker
John Palmieri, University of Washington
Session Chair
Danny Shi, University of Washington
Abstract
I will describe some of the capabilities of SageMath related to topology and homological algebra. From the topological point of view, SageMath can do basic computations with simplicial complexes, simplicial sets, cubical complexes, and semisimplicial sets, including homology and cohomology groups with various coefficients, the cohomology ring with field coefficients, and the fundamental group (modulo the word problem). It can compute mod 2 Steenrod operations on the homology and cohomology of simplicial complexes and simplicial sets. On the algebra side, SageMath has an implementation of the Steenrod algebra, commutative differential graded algebras, and finitely presented graded modules over (for example) the Steenrod algebra. I will provide examples and suggest some directions that SageMath could be expanded and improved.
11:15 AM - 12:00 PM EDT
Automatic differential propagation in spectral sequences
11th Floor Lecture Hall
Speaker
Eva Belmont, Case Western Reserve University
Session Chair
Danny Shi, University of Washington
Abstract
If you know one differential in a spectral sequence, then others can often be deduced using the Leibniz rule and other techniques. To organize this effectively on a large scale, we frame spectral sequence computation as a constraint satisfaction problem: unknown differentials are variables which satisfy constraints coming from the Leibniz rule. In the stable and unstable Adams spectral sequences, this determines a surprising percentage of the differentials. This talk discusses work by Joey Beauvais-Feisthauer and in collaboration with Francis Baer and Dan Isaksen.
12:10 - 12:15 PM EDT
Group Photo (Immediately After Talk)
11th Floor Lecture Hall
12:15 - 1:30 PM EDT
Lunch/Free Time
1:30 - 3:00 PM EDT
Group Work
Assigned Locations
3:00 - 3:15 PM EDT
Coffee Break
11th Floor Collaborative Space
3:15 - 5:00 PM EDT
Group Work
Assigned Locations
Wednesday, June 24, 2026
9:15 - 10:00 AM EDT
Introduction to homotopy type theory
11th Floor Lecture Hall
Speaker
Reid Barton, University of Gothenburg and Chalmers University of Technology
Session Chair
Benjamin Antieau, Northwestern University
10:15 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:00 AM EDT
Machine computation of the equivariant slice spectral sequence
11th Floor Lecture Hall
Speaker
Danny Shi, University of Washington
Session Chair
Benjamin Antieau, Northwestern University
Abstract
I will talk about various structures present in the equivariant slice spectral sequence, and how one could automate their computations.
11:15 AM - 12:00 PM EDT
Building mathematical databases
11th Floor Lecture Hall
Speaker
David Roe, Massachusetts Institute of Technology
Session Chair
Benjamin Antieau, Northwestern University
Abstract
I will introduce two online resources: the L-functions and modular forms database (lmfdb.org) and MathBases (mathbases.org). The first is a large database in number theory, with 20+ collections ranging from modular forms to number fields, abstract groups to elliptic curves. The second brings together an index of mathematical databases with resources for mathematicians interested in creating their own. I will aim to draw lessons that are applicable to databases in homotopy theory. Bring a laptop so that you can explore during the talk!
12:15 - 1:30 PM EDT
Lunch/Free Time
1:30 - 3:00 PM EDT
Group Work
Assigned Loctions
3:00 - 3:15 PM EDT
Coffee Break
11th Floor Collaborative Space
3:15 - 5:00 PM EDT
Group Work
11th Floor Lecture Hall
Thursday, June 25, 2026
9:30 - 10:00 AM EDT
TBA
11th Floor Lecture Hall
Speaker
Achim Krause, University of Oslo
Session Chair
Eva Belmont, Case Western Reserve University
10:15 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:00 AM EDT
Efficient computations of Yoneda product of Ext groups
11th Floor Lecture Hall
Virtual Speaker
Weinan Lin, Fudan University
Session Chair
Eva Belmont, Case Western Reserve University
Abstract
In this talk we introduce an efficient algorithm to compute the Yoneda product of Ext groups. The new program that computes the multiplicative structure of the Adams E2 page of the sphere (t<=261) is more than 400 times faster than the original program written by the speaker.
11:15 AM - 12:00 PM EDT
TBA
11th Floor Lecture Hall
Virtual Speaker
Andrew Blumberg, Columbia University
Session Chair
Eva Belmont, Case Western Reserve University
12:15 - 1:30 PM EDT
Lunch/Free Time
1:30 - 3:00 PM EDT
Group Work
Assigned Locations
3:00 - 3:15 PM EDT
Coffee Break
11th Floor Collaborative Space
3:15 - 5:00 PM EDT
Group Work
Assigned Locations
Friday, June 26, 2026
9:30 - 10:00 AM EDT
Reflections on my original design goals for Ext and how it turned out
11th Floor Lecture Hall
Speaker
Robert Chatham, Cloudflare
Session Chair
Zhouli Xu, UCLA
Abstract
My original goal in making the Ext software was to replicate the features present in Bob Bruner's and Amelia Perry's resolvers but to distribute the software in a way that was more flexible and easier to use. In particular the constraints were:
1. For performance reasons, use a "low level" performance-oriented programming language.
2. For research purposes, it should admit high performance use-cases.
3. Most mathematicians don't like to install software so it should have a low-performance web version.
4. For flexibility and ease of experimentation, it needs ergonomic bindings to a dynamic scripting language (I chose Python).
5. Ideally, the web version should also include the scripting language.
This turned out to be a rather greedy set of constraints. In the end, trying to make condition (5) work turned into a viable career for me. I will also describe my thoughts on the problem of mathematics software maintenance, and whether language model tools could make ambitious math software projects easier to maintain.
10:15 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:00 AM EDT
Formalizing the proof of the last Kervaire invariant problem with Lean
11th Floor Lecture Hall
Virtual Speaker
Guozhen Wang, Fudan University
Session Chair
Zhouli Xu, UCLA
Abstract
The Kervaire invariant one problem in dimension 126 is solved by Lin-Wang-Xu using elaborated computational techniques, showing that h6^2 is a permanent cycle in the Adams spectral sequence. In the talk, we will present the ongoing project of formalizing the proof with Lean4. We expect this would provide a template to formalize the computations in homotopy groups. In particular, the foundational theorems which are formalized in the way, such as spectral sequences, would facilitate future projects.
11:15 AM - 12:00 PM EDT
Effective spectra
11th Floor Lecture Hall
Speaker
Benjamin Antieau, Northwestern University
Session Chair
Zhouli Xu, UCLA
Abstract
I will discuss my joint project with Achim Krause to build software in which to make effective computations in the infinity-category of spectra. This talk will focus on the main theoretical results that go into the framework, the implementation we've done, and the remaining challenges.
12:15 - 1:30 PM EDT
Lunch/Free Time
1:30 - 3:00 PM EDT
Group Work
Assigned Locations
3:00 - 3:15 PM EDT
Coffee Break
11th Floor Collaborative Space
3:15 - 5:00 PM EDT
Group Work
Assigned Locations
Request Reimbursement
This section is for general purposes only and does not indicate that all attendees receive funding. Please refer to your personalized invitation to review your offer.
- ORCID iD
- As this program is funded by the National Science Foundation (NSF), ICERM is required to collect your ORCID iD if you are receiving funding to attend this program. Be sure to add your ORCID iD to your Cube profile as soon as possible to avoid delaying your reimbursement.
- Acceptable Costs
- 1 roundtrip between your home institute and ICERM
- Flights on U.S. or E.U. airlines – economy class to either Providence airport (PVD) or Boston airport (BOS)
- Ground Transportation to and from airports and ICERM.
- Unacceptable Costs
- Flights on non-U.S. or non-E.U. airlines
- Flights on U.K. airlines
- Seats in economy plus, business class, or first class
- Change ticket fees of any kind
- Multi-use bus passes
- Meals or incidentals
- Advance Approval Required
- Personal car travel to ICERM from outside New England
- Multiple-destination plane ticket; does not include layovers to reach ICERM
- Arriving or departing from ICERM more than a day before or day after the program
- Multiple trips to ICERM
- Rental car to/from ICERM
- Flights on a Swiss, Japanese, or Australian airline
- Arriving or departing from airport other than PVD/BOS or home institution’s local airport
- 2 one-way plane tickets to create a roundtrip (often purchased from Expedia, Orbitz, etc.)
- Travel Maximum Contributions
- New England: $350
- Other contiguous US: $850
- Asia & Oceania: $2,000
- All other locations: $1,500
- Note these rates were updated in Spring 2023 and supersede any prior invitation rates.
- Reimbursement Requests
Request Reimbursement with Cube
Refer to the back of your ID badge for more information. Checklists are available at the front desk and in the Reimbursement section of Cube.
- Reimbursement Tips
- Scanned original receipts are required for all expenses
- Airfare receipt must show full itinerary and payment
- ICERM does not offer per diem or meal reimbursement
- Allowable mileage is reimbursed at prevailing IRS Business Rate and trip documented via Google Maps PDF
- Keep all documentation until you receive your reimbursement!
- Reimbursement Timing
6–8 weeks after all documentation is sent to ICERM. All reimbursements are reviewed by multiple Brown University offices.
- Reimbursement Deadline
Submissions must be received within 30 days of ICERM departure to avoid applicable taxes. No submissions are accepted after six months.
Projects
Spectral sequences of algebras in SageMath
John Palmieri (University of Washington)
SageMath includes an implementation of commutative differential graded algebras over a field. The proposed project will build on this to set up a framework for computations of spectral sequences of algebras. This will start with brainstorming --- what do we want such a framework to entail, what can we hope to compute, what should the interface be, what sort of input and outputs might we want? Prerequisites: for the brainstorming, a little familiarity with SageMath wouldn't hurt but is not necessary. For implementing the ideas, you need to know Python.
Equivariant algebra and Cp Mackey Functors
Ben Spitz (Indiana University Bloomington)
The CpMackeyFunctors package for Macaulay2 was recently developed by the two project leaders, together with Chan, Mudrak, Vogeli, Wang, Zeng, and Zotine. It provides computational support for working with the abelian category of Mackey functors over a cyclic group of prime order, including random constructors and the ability to compute resolutions, ext and tor. In this project, we will expand the functionality of this package to include Green functors and modules over them, equivariant ideals, and other constructions over Cp. This project is suitable for coders of all levels and anyone interested in working with computational equivariant algebra.
Mackey functors in OSCAR
Thomas Brazelton (Harvard University)
Working closely with the Cp Mackey functors project, we will port and expand existing computational methods for Mackey functors into the OSCAR framework in Julia. Using the GAP interface, we will define data types which allow us to work with G-Mackey functors for arbitrary finite groups G. This project is suitable for more advanced coders, or those who have experience in Julia.
Machine computation of the equivariant slice spectral sequence
Danny Shi (University of Washington)
This working group will focus on developing tools and methods for machine-assisted computations for the equivariant slice spectral sequence. The goal is to translate the input data of equivariant stable homotopy theory, including representation gradings, Mackey functors, slice cells, differentials, and extension problems, into forms that can be systematically computed and checked by computer. We will discuss both the mathematical structure underlying these computations and the design of algorithms that can make large-scale slice spectral sequence calculations possible. Examples will be drawn from familiar equivariant spectra such as norms of Real bordism theories and Lubin–Tate theories.
The R-motivic Adams spectral sequence
Eva Belmont (Case Western Reserve University)
The R-motivic Adams spectral sequence converges to the (2-complete) R-motivic homotopy groups of the sphere. The goal is to compute the Adams E2 page in a range using the rho-Bockstein spectral sequence. The E1-page of the rho-Bockstein spectral sequence has been computed in a large range in C-motivic terms. Prior work of Isaksen and myself suggests that the rho-Bockstein spectral sequence is highly constrained: while there isn't exactly an algorithm for determining the differentials, in practice one can determine differentials by using known structure (such as multiplications) along with comparison with the rho-localization, which says that almost all classes must participate in a differential.
The project involves turning the techniques that Isaksen and I used into a constraint satisfaction problem which can then be fed into a SAT solver (an off-the-shelf tool for solving boolean constraint satisfaction problems). A stretch goal or extension project is to do the same for the C2-equivariant rho-Bockstein spectral sequence as described by Guillou and Isaksen, which computes the E2 page of the C2-equivariant Adams spectral sequence.
The code will be written in python. Some familiarity with python will be expected, but a little focused self-study before the workshop should suffice.
The project involves turning the techniques that Isaksen and I used into a constraint satisfaction problem which can then be fed into a SAT solver (an off-the-shelf tool for solving boolean constraint satisfaction problems). A stretch goal or extension project is to do the same for the C2-equivariant rho-Bockstein spectral sequence as described by Guillou and Isaksen, which computes the E2 page of the C2-equivariant Adams spectral sequence.
The code will be written in python. Some familiarity with python will be expected, but a little focused self-study before the workshop should suffice.
Higher (dual) Steenrod algebras
Achim Krause (University of Oslo)
From the adjunction between spectra and the derived category of F_p, one gets a corresponding comonad on D(F_p). Its coalgebras can be regarded as a coherent form of comodules over the dual Steenrod algebra. While we want to eventually make this type of structure fully amenable to computer calculations, in this project we want to focus on developing software to work with its 2-categorical truncation. The resulting theory is equivalent to Baues' secondary Steenrod algebra (and its modules), serving as an important testing ground for generalizing to higher categorical level.
Programming prerequisites: Python
Mathematical prerequisites: some familiarity with higher category theory, stable homotopy theory and Steenrod operations would be ideal
Programming prerequisites: Python
Mathematical prerequisites: some familiarity with higher category theory, stable homotopy theory and Steenrod operations would be ideal
Python bindings for sseq
Hood Chatham (Cloudflare)
sseq is a software library written in Rust to compute minimal resolutions of
chain complexes over the Steenrod Algebra. It is designed to attain a compromise
between ease of use, generality, and performance.
However, Rust is not all that convenient of a language for math experimentation.
Python would be easier for most users. The goal of this project is to create
Python bindings that are sufficiently expressive to translate the Rust code
examples to Python. Alternatively, bring your favorite use case and translate
that to Python.
I am also happy to provide tutorials in the use of the core Ext libraries or to
supervise the addition of a feature.
chain complexes over the Steenrod Algebra. It is designed to attain a compromise
between ease of use, generality, and performance.
However, Rust is not all that convenient of a language for math experimentation.
Python would be easier for most users. The goal of this project is to create
Python bindings that are sufficiently expressive to translate the Rust code
examples to Python. Alternatively, bring your favorite use case and translate
that to Python.
I am also happy to provide tutorials in the use of the core Ext libraries or to
supervise the addition of a feature.