Results 2271 - 2280 of 23900

AI for Mathematics (AI4Math) is intellectually intriguing and crucial for AI-driven system design and verification. Much of the recent progress in this field has paralleled advances in natural language processing, especially by training large language models on curated mathematical text datasets. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as Lean, which can verify the correctness of reasoning and provide automatic feedback. This talk introduces the basics of AI for formal mathematical reasoning, focusing on two central tasks: theorem proving (generating formal proofs given theorem statements) and autoformalization (translating from informal to formal). I will highlight the unique challenges of these tasks through two recent projects: one on proving inequality problems from mathematics olympiads, and another on autoformalizing Euclidean geometry problems.

The advent of artificial intelligence raises an important question: Can AI assist mathematicians in solving open problems in mathematics? This talk explores this question from multiple perspectives. We will explore how different types of AI models can be trained to provide valuable insights into mathematical questions from different areas of mathematics and applied mathematics. Additionally, we will present examples of AI models specifically designed for automated theorem proving.

We will have a charter bus take participants from the Simons Institute up to SLMath.  The bus will pick up outside of Haas School of Business on Piedmont Ave.  The first trip will leave at 4:30pm and the next one will leave at 4:45pm.

To depart from SLMath after the reception, you may take the free UC Berkeley Hill line shuttle. This shuttle leaves SLMath every half hour at the following times: 5:25, 5:55, 6:25, and 7:15.  It can make stops at the following locations: Strawberry Canyon swimming pool, between the stadium & Greek Theater, and outside Evans Hall.

The shuttles that leave at 6:25 and 7:15 will go all the way to Downtown Berkeley BART.

Mathematical intuition is often sparked by examples and counterexamples. The bad news? Constructing good examples can be difficult. The good news? SAT solvers and automated reasoning tools can help. In this talk, I will demonstrate how SAT solvers can generate insightful constructions in discrete mathematics, leading to new conjectures and concrete results. Through a series of case studies, we will see how computational search can challenge intuition, suggest patterns, and even guide mathematical discovery.

Decision problems about infinite groups are typically undecidable, but many are semidecidable if given an oracle for the word problem. One such problem is whether a group is a counterexample to the Kaplansky unit conjecture for group rings, a conjecture that was open for 80 years. I will present the mathematical context and content of the unit conjecture and explain how viewing the problem as an instance of the Boolean satisfiability problem (SAT) and applying SAT solvers shows that it is not just solvable in theory but also in practice.