Lean Reinforcement

A work-in-progress research project applying Reinforcement Learning to automated theorem proving in the Lean mathematical language.

This ongoing research project explores the application of Reinforcement Learning (RL) to automating theorem proving using the Lean programming language. The goal is to develop an AI agent that can assist mathematicians by navigating the vast search space of mathematical proofs, a task that requires both intuition and complex reasoning.

This project is a deep dive into the intersection of AI, formal mathematics, and High-Performance Computing, aiming to explore the boundaries of automated proving.

The Vision

The project aims to build an RL agent capable of suggesting and completing proof steps within the Lean environment. By training on a large corpus of existing mathematical theorems (e.g., Mathlib4), the agent will learn to recognize patterns and strategies from human-written proofs. The core of the project involves:

  • AI Agent Development: Implementing and training a hierarchical RL agent, leveraging transformer architectures to model the complex relationships in mathematical proofs.
  • HPC for Training: Leveraging High-Performance Computing resources to train models on large-scale mathematical datasets.

My Role and Technologies Used

As the sole researcher on this project, advised by Herke van Hoof, I am involved in all aspects, from conceptualization and literature review to implementation and experimentation.

Core Technologies

The project is built on a foundation of Python, Lean, and cutting-edge AI libraries:

  • Reinforcement Learning: The core of the agent is being developed using RL techniques, with PyTorch as the primary deep learning framework.
  • Lean Integration: The project interfaces with the LeanDojo environment for real-time interaction with the Lean theorem prover.
  • High-Performance Computing (HPC): Training is performed on the Snellius supercomputer, utilizing SLURM for job scheduling to handle the computational load.
  • Transformer Models: A significant part of the research involves using Transformer-based models, adapted for the hierarchical and symbolic nature of mathematical proofs.

What I’m Learning

This project is a journey into highly specialized and challenging domains. Key learning experiences include:

  • AI for Formal Reasoning: Gaining deep insights into the application of advanced AI techniques to the structured and symbolic world of automated theorem proving.
  • HPC and Large-Scale Model Training: Mastering the workflow for training large models on a supercomputer, including environment management, job scheduling, and distributed computing.
  • Self-Directed Research: Driving a research project from the ground up, involving everything from problem formulation and experimental design to implementation and analysis.

How My Skills Can Help Your Business

While this is a research-focused project, the skills I am developing are directly applicable to complex business challenges that require innovative solutions:

  • Solving Hard Problems: Experience in tackling open-ended, complex problems that don’t have straightforward answers.
  • Advanced AI Modeling: Expertise in designing and implementing state-of-the-art AI models, including Transformers, for specialized domains.
  • HPC and Scalable Computing: The ability to scale computational tasks from a local machine to a powerful distributed computing environment.

If your business is facing unique challenges that require deep technical expertise and a research-oriented mindset, I have the skills to help you explore and develop novel solutions. Please feel free to contact me to discuss your project.