An AI-Focused Tactic for Language Learning

The Project

The project aims to enhance AI proof agents by developing a domain-specific tactic language for Lean, designed to better align with AI capabilities and strengths. By analyzing the structural differences between AI-generated and human proofs, the team seeks to understand the syntactic preferences of AI agents and accordingly propose more curated AI-first tactics. This work will lead to the implementation of new tactics as well as an auto-formalization model to optimize AI's symbolic reasoning and search capabilities.

The Team

Robert Y. Lewis is an assistant teaching professor in the computer science department at Brown University. His research interests relate to the formal verification of mathematics in Lean, focusing on the tactic languages used in proofs. He is a Lean Mathlib maintainer and has been involved in formal mathematics projects for 10 years.