Lean 4 Competitive Programming

This repository is a Proof of Concept demonstrating that Lean 4 is a highly performant, technically viable language for competitive programming platforms like Codeforces.

Lean 4 compiles down to heavily optimized C code. By utilizing a zero-allocation String.Pos.Raw parsing strategy, Lean 4 can achieve C++ scanf-level I/O speeds while maintaining a strictly functional, mathematically sound programming paradigm.

Benchmarks

Standard functional programming I/O (like reading massive strings or splitting lists) causes memory allocation bottlenecks. This repository solves that via a custom Scanner abstraction using fixed-width Int64/UInt64 types for zero-allocation parsing and compact array storage.

Problem 160A - Twins, N = 1,000,000 integers (macOS, Apple Silicon):

Scenario	Parse	Sort	Greedy	Total
All equal (greedy worst case)	59ms	2ms	152ms	0.43s
Random [1, 10^7]	64ms	1ms	701ms	0.79s
Sorted ascending	59ms	2ms	146ms	0.23s
Sorted descending	61ms	1ms	149ms	0.24s
Two values (1 and 2)	46ms	2ms	192ms	0.25s
One dominant coin	44ms	2ms	146ms	0.20s

Key findings:

• Sorting uses List.mergeSort (O(n log n) guaranteed). Lean's Array.qsort degrades to O(n^2) on arrays with many duplicates.
• Parse and sort are fast; the greedy loop dominates on random data due to ~293K iterations with Int64 arithmetic.

Repository Structure

• template.lean - The core "Fast I/O" Scanner template. Copy-paste this to the top of any competitive programming submission.
• examples/ - Fully solved Codeforces problems (e.g., 160A - Twins) using the Lean 4 Scanner.
• benchmarks/ - Python scripts to generate $10^6$ inputs and verify Lean's execution speed.
• Dockerfile & .sh scripts - A sandboxed Invoker environment to prove compilation and execution compatibility.

Proposed Codeforces Integration

These commands would be enough to compile and run:

	Command
Compile	lean --c=solution.c solution.lean && leanc -O3 -o solution solution.c
Run	./solution
Version	Lean 4.28.0 (via elan)

Usage / Quickstart

1. The Docker Sandbox

To verify how the worker nodes would compile and run Lean 4:

# Build the Ubuntu + Lean 4 container
docker build -t lean-cf .

# Run the container interactively, mounting your current directory
# Use --memory and --cpus to simulate CF judge resource limits
docker run -it --rm --memory=256m --cpus=1 -v "$(pwd):/sandbox" lean-cf

2. Compiling and Running Lean 4

Inside the Docker sandbox (or natively on macOS/Linux with Lean installed):

# Compile a solution (generates C code and builds with -O3)
./compile.sh examples/twins.lean

# Run with input
./twins < examples/test_twins.txt

3. Running the Benchmarks

The benchmark script supports three modes:

# Generate inputs, compile, and benchmark (default)
python3 benchmarks/benchmark_twins.py

# Generate input files only (saved to benchmarks/inputs/)
python3 benchmarks/benchmark_twins.py gen

# Compile and benchmark only (reuses existing inputs)
python3 benchmarks/benchmark_twins.py run