NO MEETUP FOR LABOR DAY Paper Reading: Lean Agents and Formal Verification

About this event

Join us for a paper discussion on latest advancements with lean agents with 3 papers: "Vero: Can AI Agents Build Formally Verified Software Repositories?", "Formalizing Mathematics at Scale" (ATLAS), and "AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory" presented by Logan. These papers cover the latest advancements in LLMs and formal verification, where automated reasoning transitions from proving isolated mathematical lines to synthesizing entire verified software repositories, translating graduate-level textbooks at scale, and formalizing the statistical foundations of machine learning itself. vero (https://arxiv.org/pdf/2608.13522) AI4SLT (https://arxiv.org/pdf/2602.02285) Atlas-Formalizing Mathematics at Scale (https://arxiv.org/pdf/2605.29955) https://github.com/sunblaze-ucb/vero https://github.com/YuanheZ/lean-stat-learning-theory https://github.com/facebookresearch/atlas-lean Silicon Valley Generative AI has two meeting formats. 1\. Paper Reading \- Every second week we meet to discuss machine learning papers\. This is a collaboration between Silicon Valley Generative AI and Boulder Data Science\. 2\. Talks \- Once a month we meet to have someone present on a topic related to generative AI\. Speakers can range from industry leaders\, researchers\, startup founders\, subject matter experts and those with an interest in a topic and would like to share\. Topics vary from technical to business focused\. They can be on how the latest in generative models work and how they can be used\, applications and adoption of generative AI\, demos of projects and startup pitches or legal and ethical topics\. The talks are meant to be inclusive and for a more general audience compared to the paper readings\. If you would like to be a speaker please contact: Matt White