Share Lean-derived problem metadata across consumers by williamjblair · Pull Request #5375 · google-deepmind/formal-conjectures

williamjblair · 2026-09-09T13:10:49Z

Publish full Lean statements in the existing data/conjectures.json, so the website and tools can read the same data.

Measured payloads — upstream baseline 10 September; fork deployment 11 September 2026

Measurement	Before: upstream	After: fork preview
`conjectures.json`, uncompressed	8.77 MB (8,765,122 bytes)	3.11 MB (3,105,385 bytes)
Declaration records	5,269	5,264
Records with Lean statement text	0	5,264
Verso HTML and hovers	Included in the catalog	Loaded per module

For example, Erdős 92's rendering JSON is 153,826 bytes. Catalog + manifest + that rendering total 3.26 MB, versus the old 8.77 MB combined catalog. This counts those JSON files only, not JavaScript, optional evidence feeds or HTTP overhead.

Sizes are decoded UTF-8 file sizes, not compressed transfer sizes or load-time measurements. The measured snapshots differ by five declarations. The fork is at integration revision eee8f2ec; its catalog digest is recorded in the published manifest.

Before — website display data · View full conjectures.json

{
  "conjectures": [
    {
      "theorem": "Erdos196.erdos_196",
      "module": "FormalConjectures.ErdosProblems.«196»",
      "categoryLabel": "Open",
      "categoryCss": "cat-open",
      "subjects": [
        {
          "code": "5",
          "name": "Combinatorics"
        },
        {
          "code": "11",
          "name": "Number theory"
        }
      ]
    }
  ]
}

After — native Lean data, including the statement · View full conjectures.json on the fork

{
  "schemaVersion": 2,
  "problems": [
    {
      "theorem": "Erdos196.erdos_196",
      "module": "FormalConjectures.ErdosProblems.«196»",
      "category": "research open",
      "subjects": ["5", "11"],
      "statement": "True ↔ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP (⇑f) 4",
      "docstring": "Must every permutation of $\\mathbb{N}$, contain a monotone 4-term arithmetic progression?"
    }
  ]
}

These are shortened Erdős 196 records from the upstream catalog and fork catalog. Other records and fields are omitted.

The website now derives display labels and loads Verso HTML, hovers, and contributors per module. The full catalog also contains module docstrings and exact source/toolchain provenance; a manifest records its digest. The existing Lake/Verso build and static hosting remain in place.

Compatibility: the filename stays the same; conjectures becomes problems. Website readers migrate in this PR. extract_names options and field meanings are unchanged. Full JSON schema.

Live preview: Fork website · Erdős 92 example. This is the qualified integration deployment (eee8f2ec), including follow-up toolkit work. It demonstrates the combined site; the later copyright/source-link review edits are covered by PR CI below.

Checked: Full PR CI passed at 3646b794, including the maintainer review fixes. Focused checks cover 37 script tests, 8 post-processing tests and 9 Node/browser tests; changed Lean modules pass --wfail. Artifact replay preserves all 1,467 module links and produces byte-identical data after the refactor. The final fork qualification passed deployed statements, hovers, source links, fresh desktop/mobile containment, CLI browsing and website-only snapshot reuse. Upstream deployment awaits acceptance.

CLI: #5386 consumes this same catalog for conjectures find and show.

No prerequisite PR. Unblocks #4828 (including the consolidated proof-link checker) and #5386; the first production deployment must run the full build.

Fixes #5152. Roadmap: #4394.

…metadata

danielchin

This is just a first pass for minor fixes, I still have to look at this more deeply

danielchin · 2026-09-11T10:46:09Z

@@ -0,0 +1,46 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.


Suggested change

Copyright 2025 The Formal Conjectures Authors.

Copyright 2026 The Formal Conjectures Authors.

Same with all other new files

Fixed in 3646b7949. All three new Lean files now use 2026; existing files retain their original copyright year. The changed metadata modules and fixtures pass lake --wfail build.

danielchin · 2026-09-11T10:47:59Z

+def categoryToString : Category → String
+  | .textbook => "textbook"
+  | .research .open => "research open"
+  | .research .solved => "research solved"
+  | .test => "test"
+  | .API => "API"


Don't we have more categories than this?

I think undergrad and high school are a few others. You may want to search for the rest of the list.

I checked the current Category definition and parser: textbook covers high-school, undergraduate and graduate problems. The other cases are research open, research solved, test and API. This match is exhaustive over that Lean type; no category is omitted.

danielchin · 2026-09-11T10:53:42Z

+  Arxiv:               { name: 'arXiv',                    url: 'https://arxiv.org/archive/math' },
+  Paper:               { name: 'Papers',                   url: null },
+  Books:               { name: 'Books',                    url: null },
+  WrittenOnTheWallII:  { name: 'Written on the Wall II',   url: null },


I believe this is the original website but it's not loading for me right now: https://cms.dt.uh.edu/faculty/delavinae/research/wowII/

Added this URL to the collection metadata in 3646b7949. The problem modules already cite the same source path. The HTTPS endpoint also timed out in my check, so this records the cited source rather than asserting reachability.

danielchin · 2026-09-11T10:54:21Z

+const CATEGORY_META = {
+  'research open':    { label: 'Open',          css: 'cat-open' },
+  'research solved':  { label: 'Solved',        css: 'cat-solved' },
+  'textbook':         { label: 'Textbook',      css: 'cat-textbook' },
+  'test':             { label: 'Test',          css: 'cat-test' },
+  'API':              { label: 'API',           css: 'cat-api' },
+};


Similar to my other comment, I believe there's more categories.

The JavaScript table covers the same five serialized categories as the current Lean type. High-school, undergraduate and graduate problems share textbook; there are no separate current keys for those levels.

danielchin · 2026-09-11T10:57:12Z

 ```
 data/
-  conjectures.json        # JSON produced by lake exe extract_names (created by CI)
+  conjectures.json            # Complete native catalog with exact provenance


nit: fix comment indent to match the rest of the lines

Fixed the alignment in 3646b7949.

…metadata # Conflicts: # site/build.js

williamjblair · 2026-09-16T22:48:13Z

@danielchin I merged main into this branch. There was one conflict in site/build.js, and I applied the Millennium key rename from #5849 to both collection tables. All checks pass at 513b804aa, including the full Lean build. Ready for the deeper pass whenever you have time.

bocowgill

The generated catalog drops unresolved proposition answers despite declaring answer_mode: "postpone". Please fix this before merging; the inline comment documents the mismatch in the current CI artifact.

I independently checked @danielchin's category question and agree with the reply: the five serialized categories exhaust Category, with textbook covering high-school, undergraduate, and graduate problems.

bocowgill · 2026-10-09T01:31:45Z

          mkdir -p site/data
-          lake exe extract_names --exclude=statement,docstring,moduleDocstrings,fileFirstAdded,fileLastModified \
-            > site/data/conjectures.json
+          lake exe extract_names --exclude=fileFirstAdded,fileLastModified \


[P1] Preserve postponed answers until catalog extraction

Please extract the catalog immediately after FormalConjecturesAnswerPostpone, or rebuild that target immediately before this command. The intervening FormalConjectures:literate build recompiles the same problem modules in the default answer mode. In the current run's native-catalog artifact, Erdos196.erdos_196 has answerKinds: [] and a statement starting True ↔, although its source uses answer(sorry) and the manifest declares answer_mode: "postpone". Consumers therefore lose the distinction between an unresolved question and a supplied positive answer. Add an end-to-end assertion that an unresolved proposition answer still yields ["Prop"] after the full documentation/extraction pipeline.

bocowgill · 2026-10-09T01:32:16Z

+awaiting-author

Share Lean-derived declaration metadata without changing schema 2

4bead4c

github-actions Bot added the CI label Sep 9, 2026

Publish the native catalog alongside the website projection

abda07a

This was referenced Sep 9, 2026

Deliver the unified FC contribution toolkit #5376

Open

Display contribution evidence and queue context on FC pages #5377

Open

github-actions Bot added documentation Improvements or additions to documentation website javascript Pull requests that update javascript code labels Sep 9, 2026

Share schema-2 metadata validation with direct consumers

e514dfe

williamjblair marked this pull request as ready for review September 9, 2026 14:39

williamjblair added 9 commits September 9, 2026 17:29

Publish complete native catalogs with exact source provenance

b202674

Include shared import modules in catalog source cleanliness checks

decee51

Link website sources to the exact catalog revision

cf67403

Merge remote-tracking branch 'origin/main' into codex/shared-problem-…

f5c070f

…metadata

Use one native catalog with module-scoped Verso rendering

bf899f6

Keep conjectures.json as the canonical public dataset

e17ffb6

Allow explicit full fork previews after build and script checks

705531e

Preserve exact links and validate every shared catalog input

b766328

Check shared root inputs before catalog and Verso publication

658973a

williamjblair mentioned this pull request Sep 10, 2026

ci: reuse queue-built websites while preserving Lean cache refresh #5461

Draft

williamjblair added 2 commits September 10, 2026 17:06

Validate complete catalogs and preserve Verso navigation in previews

a29651d

Share snapshot validation and simplify site build orchestration

0f45902

williamjblair mentioned this pull request Sep 10, 2026

Display contribution evidence on problem pages #5388

Draft

williamjblair requested a review from Paul-Lez September 10, 2026 17:32

williamjblair requested a review from danielchin September 11, 2026 10:34

danielchin reviewed Sep 11, 2026

View reviewed changes

williamjblair added 2 commits September 11, 2026 12:29

Keep native statements within narrow page widths

dce44cd

Address metadata review documentation and source-link nits

3646b79

Merge remote-tracking branch 'origin/main' into codex/shared-problem-…

513b804

…metadata # Conflicts: # site/build.js

bocowgill suggested changes Oct 9, 2026

View reviewed changes

github-actions Bot added the awaiting-author The author should answer a question or perform changes. Reply when done. label Oct 9, 2026

		@@ -0,0 +1,46 @@
		/-
		Copyright 2025 The Formal Conjectures Authors.

	Copyright 2025 The Formal Conjectures Authors.
	Copyright 2026 The Formal Conjectures Authors.

Conversation

williamjblair commented Sep 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

danielchin left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

williamjblair commented Sep 16, 2026

Uh oh!

bocowgill left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

bocowgill commented Oct 9, 2026

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

williamjblair commented Sep 9, 2026 •

edited

Loading