A note on sources first. The recording for this session comes in two chunks: about three minutes of Pat Shafto (DARPA) announcing the four breakout groups, then a jump of roughly an hour and three-quarters to the reconvened report-out and closing town hall. The breakouts themselves ran in parallel in-person rooms and weren't filmed. So the report-out sections below are Pat's summary of each group's slides, expanded and corrected in real time by group members from the floor.
Setting up the four groups
Pat opened by framing the session as working groups: get people talking about "proposed directions, things that we can do individually and collectively to move forward toward the futures that we want" in organizing and formalizing mathematical knowledge. Four groups, in-person with a parallel online track: (1) Research and Infrastructure Roadmap, led by Daniel Spielman (Yale); (2) Funding and Coordination Strategy, led by Ken Ono; (3) Community and Ecosystem Development, announced as led by Colleen Robles (Duke) but with Dimitri Shlyakhtenko (UCLA) stepping in to lead — Pat caught the handoff mid-sentence ("Ah, Dima's stepping in. All right. Sorry."); and (4) High-Stakes Domain Applications, led by Andrew Blumberg.
The ask for each group was explicitly not an official document — "a short document outlining ideas, concrete actions that we could take toward the goals that we think are desirable," goals as well as concrete steps, to be shared back out to the whole group at the end. For the practicalities, Pat handed off to Sam, who explained that virtual attendees would get a parallel Google Form (same template as the in-person groups) linked through the Slido embed under the webcast, open until 2:30, with a smaller free-text option in Slido itself for people who just wanted to leave a quick note; virtual attendees were told to come back at 3:15. That's the entire televised record of the breakout setup. Then the tape jumps to, people taking their seats again, and Pat opening report-out.
What Pat said the groups actually reported
Pat was upfront about the nature of what followed: "I will have been brief, but we can call this vibe presenting, I suppose, since I was not there for all of the individual talks. But I'll give high-level overviews from the slides produced in each of the groups." He noted the slides would be shared out afterward, and that an open town-hall discussion would follow the report-outs. So what's below is Pat's synthesis of slide content, corrected and expanded in real time by group members who spoke up — worth keeping in mind as a filter on everything that follows.
Research and Infrastructure Roadmap
First up. The group's headline theme was reducing barriers to entry — concretely, "learning to read Lean," with Pat drawing the analogy to the old foreign-language requirement in math PhD programs (not all departments still have it, but Lean could occupy a similar structural slot), plus structured courses or teaching formats to get students, faculty, and researchers reading Lean, and better open-source autoformalization infrastructure so people are editing reasonable machine-produced code rather than writing it from scratch.
Second theme: reducing the old-mathematics backlog. Formalizing a textbook is reportedly doable at "a reasonable cost of around 10K if the prerequisites exist in Lean" — and unlike most of this post, this one is directly slide-confirmed: the group's slide reads, verbatim, "Formalizing textbooks costs ~10k if the pre-req is already in LEAN," names the two resulting artifacts as the repository and the book text with Lean embedded, and flags the barrier as "copyrighted textbooks; few textbooks are truly free." There's still real work implied in building out the prerequisite chains book-by-book. On the publication-restriction problem, the group apparently proposed a clever workaround beyond what's on the slide: hand publishers back a formalized version of their own existing textbook while simultaneously landing the formalized result in Mathlib — getting the content into the open commons without a direct confrontation over publisher rights.
Third: "infrastructure for meta-programming," which Pat flagged as having generated "a little bit of debate" in the breakout that he deferred to the town hall rather than summarizing himself. Fourth: interfaces between Lean and other proof languages — Pat named "Roc and Isabelle and Agda and Hol" as the others in this space, and the slide resolves the first name: it reads "ROCQ communities, for instance, aren't necessarily interested in integrating" — Rocq being the current name for the proof assistant formerly called Coq (renamed in 2024), not some novel or mystery language. Pat's spoken point matched the slide's framing: software verification often happens at the hardware level and won't interface with Lean, "a little bit of antibodies across the communities" toward collaboration, alongside a caution against forcing a monoculture since different languages "facilitate different ways of thinking."
Fifth: credit — establishing recognition for Lean development that can be ported into academic contexts (tenure files, grant records) and explicitly highlighted in recommendation letters for students and postdocs. Tied to this was what Pat called "quite clever": treating Mathlib itself as a potential journal-equivalent process, since it already has a built-in review pipeline — "why not elevate it a little bit more?" From the floor, this got extended into an overlay model — the kind of thing people have discussed for arXiv overlay journals, applied instead to Mathlib, where the formalization becomes part of Mathlib with its existing review process, but a package built on top could carry something closer to standalone publication status.
Shlyakhtenko added a point not on the original slide: alongside reducing the old-math backlog, there's a case for experimenting with alternate axiom systems in Lean — different versions of choice and other foundational choices some mathematicians care about — which becomes practically unavoidable if you want to formalize textbooks built on different logical systems or forcing arguments, and which raises an open question about what happens to Mathlib once you start doing that; it "goes nicely... with the other languages" point above. A second unnamed floor contribution reframed the backlog problem at the curriculum level rather than the textbook level: instead of formalizing books one at a time, formalize the full open-courseware curriculum of mathematics, on the logic that the best-positioned people to do formalization are the ones who already learned the material — there's apparently an early-stage project doing exactly this.
Community and Ecosystem Development
Second group up — announced under Colleen Robles, with Dimitri Shlyakhtenko stepping in to lead. Its first thread was best practices for publishing and disseminating AI-assisted mathematics — already being experimented with in the wild, Pat said, citing "distance conjectures signed by OpenAI, rather than a particular author" as a live case of the open question of how to credit AI relative to human co-authors. The slide's corresponding bullet is the generic "Best practices for publishing and dissemination of AI-assisted math," with no named example.
Second thread: engagement with "non-traditional mathematicians." Pat initially wasn't sure what the group meant, and the room clarified with an example — that, as the speaker put it, the Jacobian conjecture had recently been resolved by Levent Alpöge, someone mathematically trained but working outside a traditional academic mathematics post. The broader point, once untangled from that specific example, was about increasing attention to mathematics from people not embedded in it full-time — "amateurs including," in Pat's words — and how not to lose them: citizen science exists in other fields, and the room pointed to Erdős problems as an existing example of exactly this kind of harnessing in mathematics already.
Third thread, explicitly traced back to "Terry's talk" (Tao, from the prior day) and echoed "several times" since: a shift from a theorem economy — credit for proving a result — to an understanding economy, which Pat connected to needing to be more explicit about crediting the work of explaining a theorem, not just proving it. Fourth: understanding how to use AI more effectively, which Pat called "a very much moving target" as models update and interaction patterns shift, covering both how researchers collaborate with these tools and how to teach students to use them without shortchanging their own understanding of the underlying math. Fifth and sixth: cooperation between industry, academia, and government, and outreach to adjacent scientific communities, with statistics and physics named as the most proximal candidates.
Pat then caught himself having skipped two items from his notes. One: a proposal for some kind of standardizing body for certification — since various companies already pitch systems for certifying proof correctness or software correctness with varying degrees of openness, and the suggestion was that something like NIST (the National Institute of Standards) could get involved. Two, more informal: simply that people enjoyed the meeting enough that there should be some mechanism — an email list or similar — for staying in touch with people met in person here.
Funding and Coordination Strategy — and the meeting's sharpest disagreement
Third group, led by Ken Ono. Pat described the group's output as three bins. First, people: resources for junior researchers to engage with formalization, and training people in other fields to formalize their own work — which Pat noted could dovetail with senior researchers doing the same kind of work. Second, computational resources — and here Pat flagged "a feeling here that academia doesn't want to be dependent on tech companies" (the slide's own wording: "We can't have academia dependent on tech companies"), alongside a suggestion of access to DOE supercomputers (Pat was explicit he wasn't the authority to endorse that) and funding to build university compute clusters, with "Cal Compute" named as an example — confirmed on the slide as "CalCompute."
This is where the report-out turned into live, unresolved debate rather than a neat recap. One participant pushed back hard on the framing itself: academia already depends on tech companies constantly — GitHub (Microsoft-owned), email (Outlook/Microsoft or Gmail/Google) — and reached for a quote attributed to the president of SIAM (the Society for Industrial and Applied Mathematics) from "the early '90s": "mathematics is super useful. Mathematicians are useless." The same speaker then sharpened the actual worry: it's not about disliking tech — "I want more tech" — but about whether academia has a stake in building the tools rather than just consuming donations after the fact, and whether AI research direction ends up dictated by whoever controls compute and institutional AI know-how.
A second speaker, describing themselves as a co-author of the group's document, sharpened this further: Google isn't leveraging Gmail's ubiquity to steer academic research agendas, but tech companies today are actively using their control of compute and know-how about building large-scale AI systems to shape what AI researchers work on — a dynamic they explicitly want to push back against, while disclosing a seat on the NAIRR advisory board as their own point of engagement on the policy side. A third voice offered a more structural counter: every country needs a scientific policy, and in the US it's a "perfectly legitimate reality" that private-sector application and profit are a major driver of research direction. Pat tabled the thread for the closing discussion, calling it "a touch point" that "accurately reflects where things are" — real tensions and anxieties whose precise shape "is not always clearly articulated."
Returning to the group's slide content: coordination strategies included figuring out how companies and academics on different timelines can work on non-overlapping problems, protecting (for instance) graduate students from having their problem scooped — something Pat said is already done informally in the math literature — and a not-yet-publicly-announced initiative from the Mathlib maintainers called "Project Intentions," a registry where people can post plans to work on something in the Lean formalization world specifically to help deconflict. The group also flagged the harder question of deciding which problems are worth investing in even with abundant AI-assisted resources, and called for standardized data-sharing protocols to keep mathematics open, sustainable, and cumulative going forward.
High-Stakes Domain Applications, and the submissions that came in online
Fourth and, per Pat, "a much more succinct group": high-stakes domain applications, led by Andrew Blumberg. Three points: build a means for continued collaboration (contact-sharing, but "being more creative and conscious" about next steps beyond that); build a simple, effective proof-of-concept prototype aimed at outside communities — statisticians, physicists, "name your favorite community" doing work that's both important and potentially high-stakes — to entice buy-in; and, turned back on mathematics itself, the observation that the highest-stakes case for formalization may come from convincing other fields they need it, but that it's also worth mathematicians asking what they themselves need from their own foundations.
Pat then read out a separate batch of ideas submitted through the online/Slido channel described in the opening logistics. These included: a request for access to open-weight models, framed against a point raised on an earlier panel that the US "hasn't been producing... competitive" open-weight models; a request to build up Mathlib and Lean infrastructure at the National Labs, which Pat tied to "some recent announcements from DOE" people had mentioned; sponsoring free online summer schools to teach Lean to US mathematicians "at any level," with Pat noting several math institutes already run comparable programs — he named ICARM and ICERM as two separate institutes in near succession, plus SLMath (formerly MSRI), AIM, and IAS.
A "math ambassadors" idea prompted Pat to call on "Matt" from ICARM directly, who described one of ICARM's actual features: in-house technical experts fluent in Lean and other computer-aided-reasoning tools who are not machine-learning researchers but "mathematicians at heart" — three of them currently — who help visiting mathematicians get set up with the right tooling immediately rather than losing a week spinning up, accessible via short-term collaborative visits (details on ICARM's website) as well as summer schools and workshops. Pat suggested this ICARM model could extend to other disciplines down the road. The remaining online submissions: building libraries of verified compiled code, which Pat thought realizable in the short term "if people are excited about it," and changing academic incentives to recognize contributions to formal mathematics — echoing the credit theme from the research and community groups.
The closing town hall: credit, culture, and where a Lean proof should live
Pat opened the floor, noting the town hall had effectively already started during the funding-group tension, and mentioned a question queued up on a platform referred to in the transcript as "Frontier."
The first floor comment went straight at the credit question, from someone describing work with a project called "FSLib": the biggest reason people decline to contribute formalization code, in this person's experience, is fear of getting no academic credit for it under the current system — which both fails to reward existing contributors and actively deters new ones from joining these projects. The ask: a real commitment from grant-makers, institutions, or hiring committees to weigh formalization contributions on par with publications, whether through something formal — the speaker invoked "a similar type of Leiden Declaration," a likely nod to the Leiden Manifesto on research metrics — or something less formal.
A second speaker split this into two separate things being conflated — incentive (why you do math or prove a theorem: because you want to know if something's true) versus recognition (why you publish: because of the credit) — arguing the working group's ask was really about recognition specifically.
A third speaker, self-described as having sat on hiring committees and served as a department chair, pushed back on the practicality of the ask: real hiring and tenure decisions are already flexible enough to credit unconventional work if a department values the candidate, so empty declarations — the hypothetical example given was "UCLA announces that effective January 1st, 2027, we will recognize three PR contributions as the same as a paper in the Antarctica Journal of Mathematics" — accomplish little without concrete hiring precedents to point to; in this speaker's view the actual constraint is a lack of resources, not a lack of messaging, though they were open to being shown otherwise.
That drew a direct rebuttal from a speaker describing 20 years as a professional mathematician at CNRS followed by a senior corporate role, with a spouse currently on math faculty: in this speaker's view the issue is culture, not policy. Mathematics as a field is unusually resistant to change relative to, say, computer science or statistics splitting off from math departments historically — a point tied back explicitly to a remark the president of the Simons Foundation made "yesterday" about physics departments periodically shedding subfields. The speaker's diagnosis: there's a cultural perception in mathematics that if you don't prove theorems you don't belong in a math department, extending to how open-source code contributions and math education are valued, and that changing this requires role models, concrete examples, and department chairs willing to fight internal committees on behalf of atypical candidates for the sake of the field's future rather than short-term self-preservation.
The discussion then pivoted to a sharper, more concrete question from the floor: should a Lean formalization itself — independent of any accompanying paper — be submitted to arXiv as its own distributable object, and if so, what would it need to contain, as distinct from a paper that merely attaches a Lean proof as an afterthought? One answer, credited to work the speaker had done "with Sabrina... a couple of months ago": for formalizations landing in something like Mathlib or another shared project, the natural artifact to submit is the commit — specifically the diff against what existed before, plus an abstract summarizing why the contribution matters. The questioner immediately pressed for a simpler yes/no ("this is way too complicated. Yay or nay?") on whether formalizations need to be distributed rapidly and efficiently, got a "yes," and pushed further on discoverability — how would anyone find them. The resolution that emerged: no, the Lean artifacts themselves shouldn't be bundled directly into papers. The more established (if underused) pattern instead is writing a natural-language paper about the interesting mathematics and challenges that arose during a formalization — that paper goes on arXiv and then to one of a "limited number of venues" that publish this kind of work, a genre Pat said has "generally been not highly valued" and which changing the culture should mean valuing more, alongside a call for more venues willing to publish it.
The last exchange looped back to culture. One speaker reiterated that a department that respects and wants a candidate will find a way to make the hire regardless of where their work is published — arXiv, Annals, GitHub, or nowhere at all — while a department that isn't impressed won't be moved by twenty papers in traditional venues either; the real lever, again, is culture and openness to new things, and culture changes when people change — both individually and through generational turnover, as when a shrinking department under stress either makes defensive, self-preserving hiring choices or, if its members think strategically about the field's future, treats the moment as "an amazing opportunity" to reform. The closing note on this thread was a call to advocate for more resources now, "given all the publicity... and given all the good news that are out there."
Closing
With that, Pat called time — citing the need to get people to "trains and planes and automobiles" (with a nod to the movie) — and closed the entire two-day meeting with a single message: do what you think is important at every level, and if you think formalization matters, work on it; good work gets rewarded one way or another. He thanked the National Academy of Sciences for hosting, named NAS staff Sam, Brittany, Emily, and Blake, plus Ben and Kevin, thanked all the speakers and panelists across the two days, and thanked everyone who attended in person and online, closing with a hope that people leave with new ideas, new contacts, and new resources, and that they stay in touch and make use of them.
That was the final session of the two-day meeting — the town hall discussion above is genuinely where the substantive back-and-forth of the whole event landed, on the unresolved and apparently still-live question of how mathematics as a field will actually credit and reward formalization work, not just fund or build it.