Algo2Lean — Algorithms to Lean proofs

From algorithms to Lean proofs.

Write an algorithm in a typed, Python-like language. Generate its Lean definitions, then prove properties of its outputs, intermediate states, and running time.

Choose an example or open a file.
Compile and explore the Lean interface.
Write and check a proof in Lean analysis.

Click a code box to scroll inside it; press Esc to return to page scrolling. Drag its lower-right corner to resize it.

.algo

Source

Algorithm definitions

Not generated

Outputs and execution semantics. This file stays identical when only line names change.

A precise meaning for the algorithm

Compile to generate an output relation for each function. Nonterminating executions have no valid output.

Named-line interface

Not generated

Imports the algorithm definitions and adds locations and local observations for your proofs.

Name the steps you want to reason about

Put # @name on its own line directly above a statement, at the same indentation. It names the state before that statement. Compilation puts its proof interface in this separate file.

Lean Interface

Ready to compileLocal draft

Compile your source to describe its valid inputs and outputs in Lean.

Lean checker output

Shared Lean library

The algorithm definitions import Algo2Lean. Keep the library in your Lean project, or export the algorithm definitions with the library included. The named-line interface stays in its separate file.

Verify generated files

Earlier compiler versions

Open the original .algo source or project above, then select the claimed generated .lean files. All generated algorithm, named-line, and linking files must match exactly; shared libraries are also checked when selected. Exclude handwritten proofs. For module projects, choose their generated folder to preserve paths.

An exact match identifies the compiler output. It does not check a Lean proof or prove the compiler's semantics correct.

Lean analysis

Not checked

Write theorems here, then check them against the current source.

Analysis checker output

About Algo2Lean

Algo2Lean connects readable algorithm code with Lean's proof language. It supports mathematical integers, shared mutable sequences, classes, imports, and explicit cost counters.

Compilation defines the algorithm's behavior. Correctness and running-time guarantees come from the Lean proofs written against those definitions.

How compilation and checking work

This editor uses a Python compiler on this computer. Source is sent to that local server when compiling or checking; Lean checking requires a local Lean installation. Draft recovery uses browser storage. Save or download files for a durable copy.

The language is a defined Python-like subset. Lean checks the generated definitions and submitted proofs; this does not itself prove that the compiler implements the intended language semantics.

Cite Algo2Lean

If Algo2Lean contributes to a paper or formalization, please cite the software and record the compiler version used.

Loading citation details…

BibTeX

This is a development build. For published work, use the citation for the exact release.

Algorithm and proof authors retain credit for their work.