A quick note on how this one is attributed: unlike the single-speaker talks in this series, a panel transcript doesn't reliably tag who's talking turn by turn. I'm reconstructing attribution from the panelists' self-introductions, their agency-specific vocabulary (NSA's "isolated networks," NSF's grant mechanisms, NRL's "embedded mathematicians"), and the moderator's apparent habit of calling on people in the same order he introduced them. Where I'm confident, I name the speaker directly; where I'm not, I say so.
Three agencies, three ways into the room
Coming back from the mid-morning break, the moderator — Pat Shafto of DARPA, who reveals at the very end that he's a program manager "on loan from Rutgers" — frames the session as "a discussion on federal perspectives on these questions of infrastructure for mathematical knowledge", then has the three panelists introduce themselves in turn. The panel runs without slides — the projector screen stays blank throughout — and the panelists are identified only by tent name cards on the table.
Mike O'Hara goes first: chief of mathematics research at NSA, with a background spanning cybersecurity, data science, and cryptanalysis. His one piece of "color commentary": in graduate school he was in an applied math program and picked AI as his application area, then gave it up after a couple of years for quantum computing "because I just didn't feel like I was learning enough" — a choice he now finds "really funny," given where AI has gone since.
Stacey Levine introduces herself next. She's a program director in the mathematical sciences at NSF, with applied mathematics as her core program and a hand in computational math as well. She names two specific NSF initiatives she's involved in at the math/AI interface — the Mathematical Foundations of AI program and the AI Formal Methods and Mathematical Reasoning program, the latter of which she says "aligns very well with this particular workshop" — plus a role on the Mathematical Sciences Research Institutes team. Her own training is in PDEs, specifically harmonic map theory, which she says evolved into image and signal processing applications and eventually pulled in machine learning.
George Stantchev closes the introductions: research scientist in computational and applied mathematics at the Naval Research Lab in DC, trained as a differential geometer working in low-dimensional topology, who's spent his career since grad school in applied and computational math. His self-description of what he does now is memorable enough to quote in gist rather than flatten: he calls it "human formalization of science," and says that having seen what formalization has done for mathematics itself, he wants to help extend that to scientific and engineering discovery more broadly.
What formalized math is for, agency by agency
Shafto's first substantive question: what role does mathematics play in your work, or what role do you play for mathematics?
O'Hara answers first, and the framing is unambiguous: "mathematics is the core competency of the National Security Agency," touching personnel analysis, data science, human languages, cybersecurity, and signals analysis. He adds his own qualified claim — "I guess we're the largest employer of mathematicians" — and notes that NSA has recruiting material ready to go for events like the Joint Mathematics Meetings, pitching itself as a great place for mathematicians to work.
Levine describes NSF's role as much broader in kind: supporting mathematics "generally," across discovery of new mathematics, training junior mathematicians, and mathematics' role in advancing science and prosperity — delivered through individual grants, cross-disciplinary and interdisciplinary grants, training awards, and institute programming. She specifically credits NSF support for the 2023 National Academies (NASEM) workshop on AI to Assist Mathematical Reasoning as an example of this outreach. She also notes NSF supports infrastructure "in different ways," some of which benefits mathematicians directly.
Stantchev's answer is the most granular of the three, and the most different in kind from the other two: he's not a funder, he's "in the trenches." At NRL he works across teams on nonlinear dynamical systems and complex network systems (extending into multi-agent autonomous systems), reduced-order models, computational materials science done "in a physics informed way" (he flags physics-informed ML/AI as "quite a bit of a theme lately"), and signal processing / applied harmonic analysis at the system level. Structurally, he notes NRL has no dedicated mathematics department or division — unlike, he says, the Department of Energy's more centralized math centers — and instead has mathematicians embedded across units, collaborating directly with domain scientists and engineers.
When models can think for a day and a half
Shafto's second question turns to formalization directly: what are the challenges and opportunities of large-scale formalization of math for the kind of work you do?
Following the established rotation, the first response — O'Hara — opens with a detour worth keeping verbatim: a reference to "our kickoff for the DARPA xMAT program in March" and a line credited to an unnamed person the speaker respects, that "we used to live in dog years, and now we live in fruit fly years" — "seven generations of fruit flies since March". (xMAT reappears at the very end of the panel as Shafto's own DARPA program, "Exponentializing Mathematics" — so this speaker is describing an event Shafto runs, not claiming to run it themselves.)
The substantive point that follows: AI is "already a fundamental tool in mathematical research," and that wasn't true not long ago. As models get more powerful, the scope of questions you can pose to them grows — weak models could only be asked narrow, quickly-computable questions, but powerful models can now "go off and think for quite a while." The catch: if a model can't check its own work and makes a reasoning error early on, "they'll think for a day and a half and just give you a mountain of fluff" — what "people call... slop," a word the speaker says he doesn't favor. His stated view of formalization's role here is specific: not primarily to build "this pyramid of verified proofs," but to expand the scope and duration of reasoning that AI agents can do autonomously on math problems by giving them a way to check their own reasoning.
The cultural blur
Levine's response to the same question is the longest sustained answer of the panel, and it moves through several registers. She opens by validating that the challenges — cultural, incentive-related, resource-related — "have been really well articulated" earlier in the day, and says as a funder NSF is "listening" and actively working out what role it, versus "sibling federal agencies," philanthropies, and industry, should each play.
She then pivots to opportunity: NSF's broad portfolio has "never dictated which emerging technologies or techniques should be used" to advance mathematics or science, and while cultural barriers exist between communities, she sees the line between them "increasingly... blurred," pointing out that four or five years ago this topic was "barely discussed" within the mathematical community and now has substantial programming and discussion behind it.
Two callbacks to earlier talks in the day follow: Ken Ono's remarks on hiring traditionally-trained mathematicians, and Terence Tao's comments on "proof digestion". She then relays a specific anecdote from side conversations with mathematicians: "even six months ago, the discussion was maybe 60% of my research is traditional mathematics, and 40% is AI-assisted mathematics," and now those same people say the line is "blurring... accelerating quite a bit".
Her closing point is about incentive structures broadly (financial, tenure-related, and the intrinsic excitement of the science) as levers that could help formalization "permeate through the community".
George's chain: phenomena to proof and back
Stantchev's answer to the same question is the panel's most technically developed single stretch, and it's worth following closely because it's effectively his thesis for the rest of the panel. He starts from a pointed observation he credits to Andrew Blumberg's talk earlier that same morning: extending formal methods, as discussed "here in this community," into applied mathematics is necessary because isolated proofs of pure-math theorems, interesting as they are, "is not going to be adequate" for applied problems. He makes the point sharply: "I'm not aware of anybody at the government research labs working on Riemann hypotheses or... the Ehrenfeucht problems" — the latter a reference to the Ehrenfeucht conjecture in combinatorics on words, a compactness result guaranteeing every language a finite test set for word equations (proved by Albert and Lawrence in 1985) — "at least not being paid to do that".
His constructive proposal is a pipeline: start from phenomena or data, move to models and idealizations, arrive at a mathematical formulation, do the theorems and proofs (and algorithms) at that level of abstraction, then move back down through implementation to predictions, discovery, or decision-making. Formal methods, he argues, belong "somewhere inside that chain," but only "if they're interfaced properly". The obstacle he names explicitly: "there's some kind of impedance mismatch" between formal methods in their current form and the rest of that chain, because most current data-driven approaches treat everything between input data and output prediction as one undifferentiated black box — which raises the question of whether a working prediction actually means the underlying model is correct, generalizes, or is safe to use in "critical applications". His call to action is directed specifically at startups working on formal methods in "strictly... pure mathematical context": reach out and hire more applied mathematicians so the fusion "can happen and grow organically from the ground up" — and he's explicit that the outreach should run from the formal-methods community outward, since he doubts people outside that community are aware of or care about formal methods on their own.
Isolated networks and the awareness gap
Shafto's third question asks about the form of formalized mathematical knowledge — technical, social, incentive structures.
O'Hara's answer is short and concrete, and distinctly NSA-flavored: "I would like to be able to import it." His agency does much of its work on isolated (air-gapped) networks, so if something is open-sourced, he wants to be able to clone it onto NSA's own network and use it — "everybody loves cloud-hosted these days, but that has limitations for us".
Levine agrees open source is "the immediate thing that comes as an answer," and stresses that for NSF's research-community mission, tools need to be not just accessible but "user-friendly" — while acknowledging this is "a challenge," requiring "a huge amount of infrastructure, huge amount of data".
Stantchev's addition is about awareness rather than access: the formal-methods community remains, in his view, "relatively small and self-contained," and applied mathematicians and scientists outside it "need to be made aware of what the potential is." He again invokes the fuzzy boundary between communities, crediting the observation to an earlier speaker. His prescription: build simple, legible worked examples that show people concretely "you can do this if you had X, Y, and Z".
Government, industry, academia: BAAs, MURIs, and the outfield
The final substantive question: challenges and opportunities of government working with industry and academia to realize these futures.
Levine answers first this time, describing a long history of government collaboration across agencies, philanthropies, and industry where missions align or resources complement each other. She states that NSF supports "25% of the federally funded, I believe" foundational research, "basic research driven by curiosity and discovery," contrasted with industry's different incentives, and points to NSF's collaboration mechanisms, including its Technology, Innovation and Partnerships (TIP) Directorate.
O'Hara's answer pivots to NSA's own posture: "historically a pretty insular organization" — complete with the agency's standard self-deprecating "no such agency" joke — but one that, given the pace of AI and math advances, doesn't operate "under any illusions" that it can match the expertise in the room alone. He calls the need for events like this one, and Shafto's DARPA program, "really urgent".
Stantchev's turn opens with a disclaimer he says he should have given earlier: he doesn't speak for the Naval Research Lab, the government generally, or the Department of Navy — these are his own views. A brief cross-talk follows — someone says "I can speak for NSF" (likely Levine, drawing a contrast with Stantchev's disclaimer), then "Right," then "Now is your opportunity, right" (likely Shafto, prompting Stantchev to continue).
What follows is Stantchev's roadmap, organized by time horizon. He advocates for government funding mechanisms — BAAs, MURIs ("although MURI's are a little tricky these days," he adds) — that incentivize collaboration and expansion of current formal methods into broader areas. Near-term, "almost immediately": software verification, where formal methods are already established territory, though he thinks the latest formalization methods haven't yet been applied there; and digital circuit design, where he relays that someone from a startup approached him at the "Xmath kickoff meeting" asking about FPGA verification, claiming they could "do it now" — he hasn't heard back since. Midterm: integrating formal methods into existing agentic frameworks, naming George Em Karniadakis at Brown and his group's ATHENA (Agentic Team for Hierarchical Evolutionary Numerical Algorithms), its GRAFT-ATHENA extension, and AgenticSciML (the transcript's "AI-SCIMLE") — a family of agentic scientific-machine-learning systems in which agent-experts propose models and others reject them, negotiated via contextual bandits. He describes them as "a good step towards formalization" but without the same guarantees as formal methods proper, and notes Karniadakis's group "has gone quite a bit in the last three, four years".
Far-term — his term is "the outfield" — he names quantum computing and quantum optics (heavy mathematical models that could benefit from formalization) and computational materials science, where formalized models could filter out discoveries that look promising in a "fuzzy space" but fail under rigorous DFT analysis or don't work in nature; he draws an explicit parallel to Andrew Blumberg's morning comments on pharmaceutical discovery.
The moderator's reveal, and a pitch for program management
Shafto closes the panel by turning the same question on himself, revealing his own role explicitly for the first time: he's at DARPA, leading AIQ ("about mathematical foundations for AI and evaluation") and Exponentializing Mathematics — xMAT, the program referenced earlier in the panel — "about AI and formalization for pure mathematics." He adds that he's "on loan from Rutgers".
He makes an explicit pitch: every agency represented on the panel hires mathematicians in some capacity, and at DARPA specifically, "no mathematicians mean no math programs" — framing the program manager role as one mathematicians should consider stepping into rather than dismissing as a detour from a research career. He ties this to the afternoon's structure: working groups where attendees will think concretely about individual and collective actions to shape the field's future, which he frames as a real opportunity rather than a formality.
Asked directly how the afternoon logistics will work, he says it will be "by self-assignment," with group leads describing their groups before everyone breaks — though the panel adjourns to lunch before that detail gets fleshed out on tape.