live_prover

Repo for proving Lean theorems via a web interface.

Overview

live_prover is a web-based tool for interactively proving theorems using Lean. This repository contains the source code for the web interface and backend integration with Lean.
This project implements the Lean web interface discussed in the paper: Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method.

Features

• Interactive Lean theorem proving in the browser
• Syntax highlighting and error reporting
• Real-time feedback from Lean
• Proof search using fixed and dynamic tactic sampling methods
• REST API endpoints for proof search and tactic generation

Getting Started

Prerequisites

• Lean installed locally

Installation

Clone the repository:

git clone https://github.com/rahul3613/leanprover_web.git
cd leanprover_web

Install Python dependencies:

pip install -r requirements.txt

Running the Server

Start the Flask server:

python server.py

The web interface will be available at http://localhost:5001/project/ds-prover/.

Usage

• Write Lean code in the editor on the web interface.
• Submit to see proof verification and feedback.

API Endpoints

• POST /project/ds-prover/prove/
  Parameters: statement (string), model, sampling
  Returns: Proof result and details.

• POST /project/ds-prover/generate/
  Parameters: goal (string), num_samples, model
  Returns: Generated tactics.

Reference

For more details, see the related paper: https://arxiv.org/abs/2312.14188