---
schema_version: "newruntime-agent-readable-v0.2"
type: "raw_signal"
stable_id: "signal:lean-zstd-proof-automation"
id: "nr-f54dc79b-9f58-4e46-8532-96e3caca804e"
slug: "lean-zstd-proof-automation"
title: "LLMs Make Lean Proofs a Retryable Engineering Loop"
description: "ImperialViolet's zstd-in-Lean experiment shows proof automation becoming practical when the model can generate attempts and Lean provides strict deterministic verification."
retrieval_nugget: "ImperialViolet's zstd-in-Lean experiment shows proof automation becoming practical when the model can generate attempts and Lean provides strict deterministic verification. The signal shifts formal methods from rare expert ceremony toward a generator-verifier loop: LLMs can fail repeatedly while Lean cheaply rejects bad proofs and accepts only type-checking ones. Novelty is structural; verification is source-inspected."
observed_at: "2026-07-28"
record_date: "2026-07-28"
date_kind: "observed_at"
why_it_matters: "The signal shifts formal methods from rare expert ceremony toward a generator-verifier loop: LLMs can fail repeatedly while Lean cheaply rejects bad proofs and accepts only type-checking ones."
novelty: "structural"
verification_level: "source-inspected"
signal_type: "operating-model"
evidence_kind: "primary-source"
status: "published"
source_platform: "curated"
source_record_id: "f54dc79b-9f58-4e46-8532-96e3caca804e"
source_url: "https://www.imperialviolet.org/2026/07/26/zstd-lean.html"
topics: ["lean","formal-verification","verification"]
entities: ["ImperialViolet","Lean","Zstandard"]
related_patterns: ["verification-bandwidth-is-the-scarce-resource","harness-architecture-outlives-model-choice","agent-ready-software-exposes-capabilities"]
source_urls: ["https://www.imperialviolet.org/2026/07/26/zstd-lean.html"]
routes: {"html":"https://newruntime.com/signals/lean-zstd-proof-automation/","markdown":"https://newruntime.com/signals/lean-zstd-proof-automation.md","json":"https://newruntime.com/signals/lean-zstd-proof-automation.json"}
source_format: "editorial-normalized-json"
---

# LLMs Make Lean Proofs a Retryable Engineering Loop

## Retrieval answer

ImperialViolet's zstd-in-Lean experiment shows proof automation becoming practical when the model can generate attempts and Lean provides strict deterministic verification. The signal shifts formal methods from rare expert ceremony toward a generator-verifier loop: LLMs can fail repeatedly while Lean cheaply rejects bad proofs and accepts only type-checking ones. Novelty is structural; verification is source-inspected.

## Observation

ImperialViolet's zstd-in-Lean experiment shows proof automation becoming practical when the model can generate attempts and Lean provides strict deterministic verification.

## Why it matters

The signal shifts formal methods from rare expert ceremony toward a generator-verifier loop: LLMs can fail repeatedly while Lean cheaply rejects bad proofs and accepts only type-checking ones.

## Provenance

This public record is a sanitized New Runtime Editorial Inbox signal. Linked source_urls carry the publishable evidence boundary; private discovery provenance stays internal.