Newsroom
Applied Mathematics
-

How to Generate and Verify LLM-Generated Lean Proofs for Your Mathematical Needs
A hands-on workshop on using large language models and Lean to formalize mathematical claims, audit generated proofs, and determine whether a machine-verified result actually says what you intended. When Lean says a proof is correct, what exactly has been proved? Large language models can translate mathematical arguments into Lean, but a proof that compiles is…
-

FDS Workshop: AI for Scientific Discovery
Recent advances in generative AI are reshaping how we design and discover mathematical and scientific artifacts. Problems in mathematics, engineering, and the sciences have recently been solved by systems that use LLMs to evolve search and optimization algorithms. If you can specify what you are looking for, they can help you find it. Concretely, LLM-guided…
-
FDS Colloquium: Steven Johnson (MIT), “Co-design of Optics & Inference”
Abstract: Over the past two decades, an explosion in fabrication capabilities for nano-structured optics has coincided with the development of powerful techniques for “inverse design” — large-scale PDE-constrained optimization, sometimes with millions of degrees of freedom, that reveals surprising irregular structures for a diverse range of devices. Light emission, sensing, communications, and imaging have all…
-
S&DS Seminar: Stan Osher (UCLA), “Recent Results on Mean Field Games, Optimal Transport, and In-Context Learning”
Abstract: We have recently been developing algorithms related to mean field games, optimal transport, in-context learning, score based generative models and links between Laplace’s method, the Moreau envelope and Hamilton-Jacobi equations. I will try to give a coherent talk including many of these. Speaker bio: Stanley Osher, Professor at the University of California, Los Angeles, serves…
