BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Leopoldo Sarra (Axiomatic AI) DTSTART:20260119T160000Z DTEND:20260119T163000Z DTSTAMP:20260420T024855Z UID:LT2026/4 DESCRIPTION:Title: T owards autoformalization for physics and engineering with Lean\nby Leo poldo Sarra (Axiomatic AI) as part of Lean Together 2026\n\n\nAbstract\nWe strive to bring formal methods and interactive theorem provers like Lean 4 to the broader scientific community beyond mathematics. To ease its adop tion\, we are building reusable Lean libraries that formalize areas of sci ence using the main concepts that scientists and engineers actually apply in practice\, such as dimensional analysis\, tolerances\, and approximatio ns.\n\nWe begin with physics domains that have a strong mathematical groun ding\, like quantum mechanics\, where we validate the correctness of the l ibraries on real use cases and problem sets (e. g. 700 problems from Galit ski et. al. 2013) to ensure their practical relevance and adoptability.\n\ nFinally\, we are developing autoformalization AI agents to further boost the adoption of formal methods in science and engineering. These agents wi ll have access to the libraries we build\, as well as Mathlib\, enabling t hem to help formalize real-world problems together with their proposed sol utions in the form of theorems. This allows us to certify the validity of a given solution by converting it into a formal theorem and proving it thr ough our prover AI agents.\n LOCATION:https://researchseminars.org/talk/LT2026/4/ END:VEVENT END:VCALENDAR