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.
Browser drafts 0
Recover a source and analysis pair to continue editing. Each tab saves separately. Drafts stay here until you discard them.
No saved drafts yet. Your edits will appear here.
Click a code box to scroll inside it; press Esc to return to page scrolling. Drag its lower-right corner to resize it.
.algo
SourceAlgorithm definitions
Not generatedOutputs 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 generatedImports 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 draftCompile your source to describe its valid inputs and outputs in Lean.
Lean checker output
Verify generated files
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 checkedProof checking is not currently available on this website. You can check the supplied proofs using your own Lean installation or an editor with Lean support. Use Save analysis to download a proof.
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.