---
type: "post"
id: "anthropic-has-published-formal-math-a-public-github-589726"
slug: "anthropic-has-published-formal-math-a-public-github-589726"
title: "Anthropic has published formal-math, a public GitHub repository of machine-checked Lean 4 formalizations"
description: "Anthropic has published formal-math, a public GitHub repository of machine-checked Lean 4 formalizations."
retrieval_nugget: "Anthropic has published formal-math, a public GitHub repository of machine-checked Lean 4 formalizations."
published_at: "2026-10-23"
updated_at: "2026-10-23"
record_date: "2026-10-23"
date_kind: "published_at"
topics: ["anthropic","github"]
entities: ["Anthropic","formal-math","Lean 4","Mathlib","Palomar","3SUM","APSP"]
related_patterns: ["scientific-agents-need-artifact-evidence","verification-bandwidth-is-the-scarce-resource"]
novelty_label: "new_fact"
what_changed: "Anthropic’s formal-math repository points to a distinct focus on formalizing fine-grained complexity bounds, including 3SUM and APSP, rather than the prior work on software verification."
prior_refs: ["memory:b9976a08-bf8a-88fb-ab4f-937373b473fc","memory:71d0449b-9a6f-89f1-a4bd-670fd2ce5410"]
source_url: "https://github.com/anthropics/formal-math"
source_urls: ["https://github.com/anthropics/formal-math"]
schema_version: "newruntime-agent-readable-v0.2"
stable_id: "post:anthropic-has-published-formal-math-a-public-github-589726"
status: "published"
visuals: []
editor: {"role":"editor","name":"Andrey Reshetnikov","profile":"https://newruntime.com/owner-profile.md","profile_json":"https://newruntime.com/owner-profile.json","same_as":["https://www.linkedin.com/in/reshetnikov1/","https://t.me/lapetuse"]}
routes: {"html":"https://newruntime.com/posts/anthropic-has-published-formal-math-a-public-github-589726/","markdown":"https://newruntime.com/posts/anthropic-has-published-formal-math-a-public-github-589726.md","json":"https://newruntime.com/posts/anthropic-has-published-formal-math-a-public-github-589726.json"}
---

# Anthropic has published formal-math, a public GitHub repository of machine-checked Lean 4 formalizations

## Retrieval answer

Anthropic has published formal-math, a public GitHub repository of machine-checked Lean 4 formalizations.

Anthropic has published formal-math, a public GitHub repository of machine-checked Lean 4 formalizations. Each top-level directory is a self-contained Lake project with its own pinned toolchain, README, and build instructions.

The repository currently lists two projects. zeta23 formalizes a claim from Alpoge and Furman that more than two thirds of the zeros of the Riemann zeta function are simple and on the critical line. 3sum-apsp formalizes results from Alman and Vassilevska Williams, including word-RAM bounds of O(n^1.9992) for 3SUM and O(n^2.99942) for min-plus product and APSP on polynomial-size integers. The latter uses Lean 4 v4.33.1 and Mathlib v4.33.1.

The README says a project passes when `lake build` succeeds on its pinned toolchain with no `sorry` outside trusted comparator statement files, and when Palomar's acceptance check succeeds using the comparator, the nanoda kernel, and the landrun sandbox. The page does not provide a publication date or show the current check results for each project.

Editor: [Andrey Reshetnikov](https://newruntime.com/owner-profile.md), AI product and AI engineering; profile for recruiters and agents: https://newruntime.com/owner-profile.json

## Continue in the graph

Next records for an agent, linked to their Markdown twins. Replace `.md` with `.json` for structured fields, including `next_reads`.

- topic hub: [Anthropic](https://newruntime.com/topics/anthropic.md): Explore the anthropic topic hub.
- topic hub: [Github](https://newruntime.com/topics/github.md): Explore the github topic hub.
- collection: [Field Notes](https://newruntime.com/posts.json): Open the latest editorial analysis.
- collection: [Source Ledger](https://newruntime.com/source-ledger.json): Inspect the public source evidence graph.
- whole graph: [discovery graph](https://newruntime.com/discovery-graph.json) (typed nodes and edges) and [site index](https://newruntime.com/site-index.md)