Skip to content

README.md

Latest commit

 

History

History
150 lines (118 loc) · 7.58 KB

README.md

File metadata and controls

150 lines (118 loc) · 7.58 KB
Raw

Formal specifications (lean-project/)

This Lake project holds the Lean 4 + Mathlib formalisations produced by formalize.py from the Hypothesis property tests written by the PBT agent. Every Python function is translated as a real Lean def (not an opaque axiom), whose behavioural equivalence to the Python original is checked by a Hypothesis-driven oracle.

What this project IS

A corpus of (Python function, equivalence-checked Lean def, theorem statements about the Lean def) triples. The theorem proofs are sorry — proving them is downstream work. The contribution is:

  1. The Lean def is faithful to the running Python on the input domain the Hypothesis strategy covers (typically 200 inputs).
  2. The theorem statements are well-formed in Lean's logic — they type-check, and they refer to the actual def (not an opaque axiom).
  3. The whole tree is enumerated in formalization_results.jsonl, with explicit status codes for every failure mode.

The artifact shape (per function)

lean-project/Spec/Properties/<Pkg>/<CallId>/
├── <Fn>.lean                       Lean def + theorems (all sorry)
├── <Fn>_Runner.lean                JSON-IPC harness for the oracle
└── translation_hole_<Fn>.md        ONLY if partial-translation gaps exist

../../../results/<pkg>/aux_files/<call_id>/
├── translation_check_<Fn>.py       Hypothesis-driven Python↔Lean oracle
├── translation_disagreement_<Fn>.md   ONLY on disagreement
└── bug_report_<Fn>_<ts>_<hash>.md  ONLY if agent suspects a Python bug

A record is clean iff lake_build_ok && translation_check_ok && some theorem is non-trivial (i.e. survives the triviality filter). Downstream prover training filters on this combined flag.

What this project IS NOT (the holes)

These are real limitations of auto-formalisation. They are not bugs. They are listed prominently so anyone reading these files knows what is and isn't claimed.

ID Hole Disposition
A1 Translation faithfulness (Lean def ≠ Python def) Closed behaviourally within a restricted input domain: oracle runs ~200 Hypothesis-generated inputs through both Python f and Lean f via subprocess + JSON IPC. Strict JSON-serializable inputs only — strategies producing numpy arrays, custom classes, recursive types, or callables produce a non_json_input_domain hole. ANY disagreement (after non-determinism check) rejects the translation.
A1b Python-side non-determinism (random, time, IO) Closed by detection: oracle runs Python f twice on each input. If Python disagrees with itself, the function is marked python_non_deterministic and the oracle is skipped. The Lean def is retained but flagged.
A1c NaN equality convention Deliberate convention: NaN-on-both-sides is treated as agreement by the oracle, even though Python == and math.isclose both return False for NaN. Rationale: both implementations correctly model "no answer here." NaN-on-one-side-only remains a disagreement.
A2 Python features (IO, mutation, exceptions, opaque types) Pure-kernel-only translation: translate the pure logic, document omitted effects in translation_hole_<fn>.md.
A3 Float / IEEE-754 vs Lean ℝ mismatch Two-tier policy in Spec/Common.lean: use IeeeFloat (= Lean Float) when the property is about IEEE-754 runtime behaviour; use MathReal (= ℝ) only when the strategy filters NaN/inf AND the property is mathematical. Leading comment in each file records the choice.
A4 Hypothesis-strategy ↔ Lean-type lossiness Documented in each file's leading comment; conventions in Spec/Common.lean.
B1 Theorem-statement correctness Mitigated, not closed — no oracle exists. Mitigations: triviality filter (B2), differential testing via refinement, sample human review via formalize_review.py.
B2 Theorem non-triviality Closed by triviality_filter.py: theorems auto-discharged by decide/trivial/rfl/simp/omega are flagged triviality_filter_ok: false and excluded from the clean corpus.
B3 Theorem-shape diversity Five buckets: pbt_mined (universal lifts of PBT equational properties), refinement (paired-impl), algebraic (monoid/group/ring laws), termination (metadata), complexity (metadata from docstring).
B4 Termination + complexity as theorems Termination is automatic for Lean def — recorded as metadata, not a theorem. Complexity is recorded as a complexity_from_docstring metadata string only — no Lean Asymptotics.IsBigO theorem is attempted (three stacked hard tasks not worth burning tokens on).
Bug Python bugs noticed during translation Surfaced as bug_report_*.md alongside the formalisation, deduped against existing /hypo reports.
D1 Proven Lean → running artifact (FFI) DEFERRED — future work. The oracle uses subprocess + JSON IPC, which validates equivalence but does not ship Lean as runtime.
D2, D3 Module composition, specs for new code Out of scope.
C1-3 Automated proving Out of scope — next project. Every theorem here is := by sorry.

Worked example

For Python's math.gcd:

# Python source
def gcd(a: int, b: int) -> int:
    """Greatest common divisor. Time complexity: O(log(min(a,b)))."""
    while b:
        a, b = b, a % b
    return abs(a)

The agent produces:

-- Spec/Properties/Math/<CallId>/Gcd.lean

/-
Property: gcd_commutative, gcd_divides_both, gcd_identity
Source: <path>
Package: math
Call ID: <id>

Translation notes:
- Python ints are unbounded; Lean's `Int` matches over the strategy domain.
- Termination: well_founded; measure: b.natAbs (decreases on each recursion).
- python_origin: bounded_loop translated as well-founded recursion.
- complexity_from_docstring: "O(log(min(a,b)))" (metadata only)
-/

import Spec.Common
import Mathlib.Data.Int.GCD.Basic

namespace Spec.Properties.Math.AbcdEf12

open Spec

def gcd : Int → Int → Int
  | a, 0 => a.natAbs
  | a, b => gcd b (a % b)
decreasing_by exact ...

-- @theorem_type: pbt_mined
theorem gcd_commutative (a b : Int) : gcd a b = gcd b a := by
  sorry -- HOLE: proof omitted by design; see lean-project/README.md

-- @theorem_type: algebraic
theorem gcd_divides_left (a b : Int) : (gcd a b : Int) ∣ a := by
  sorry -- HOLE: proof omitted by design; see lean-project/README.md

end Spec.Properties.Math.AbcdEf12

Alongside, the oracle script aux_files/<call_id>/translation_check_gcd.py runs ~200 Hypothesis-generated (a, b) pairs through both Python math.gcd and the compiled Lean def via lake env lean --run Gcd_Runner.lean, comparing JSON-encoded outputs.

Structure

lean-project/
├── lakefile.toml             Lake config; depends on Mathlib
├── lean-toolchain            Lean version pin (managed by setup_lean.py)
├── README.md                 This file
├── Spec.lean                 Root module; imports every property (auto-managed)
├── Spec/
│   ├── Common.lean           Translation conventions & helpers
│   └── Properties/
│       └── <Pkg>/<CallId>/   Per-function formalisations
└── formalization_results.jsonl   One record per (pkg, call_id, fn)

Building

# One-time setup (installs elan + Mathlib oleans):
python ../utils/setup_lean.py

# Build all formalised properties:
lake build

formalization_results.jsonl records every attempted formalisation with status, oracle outcome, theorem build outcomes, triviality verdicts, and any holes — see plan.md in the repo root for the full schema.