formal-conjectures integration

[Paul-Lez]

Just opening this issue to track discussions and work related to the integrating problem sets from formal-conjectures into Lean eval.

I think one good place to start would be the FC100SolvedSet1 and FC100OpenSet1 (100 open and solved problems - there will be more releases of such sets in the future!). The subsets can be found here

Currently the idea seems to be:

• Since these are all open problems (rather than already known theorems) they should go in a separate tab
• Unlike solved problems, making solutions public should be part of the conditions for submission of a solution.

Link to discussion on the Lean Zulip.

I'm planning on working on (prototyping) this integration, but any pointers to get started would be helpful @kim-em!

[kim-em]

The shared-generator foundation is now public at https://github.com/leanprover/lean-eval-generator, with v1 pinned at a726789593eeac5c32ad82760061cd5bf6cae662. LeanEval PR #540 consumes that exact revision. The package exposes a versioned JSON CLI/schema boundary and returns complete generated file contents plus SHA-256 digests; the consumer remains responsible for resolving hole metadata against its elaborated target environment. Representative theorem- and definition-hole workspaces have been checked byte-for-byte in a disposable regenerated tree. FC100 import remains gated on the FC-owned adapter, whole-set target-environment answer-slot audit, and dependency audit; this does not enable an import or publication by itself.

[kim-em]

The requested whole-FC100 adapter/answer-slot audit has now been reproduced against formal-conjectures PR #4951 and LeanEval target pins. Inventory is exactly 100 entries but 92 open + 8 solved, with 61 answer slots (48 Prop, 13 non-Prop). Source extraction verifies 89/100; 11 declarations fail before target generation. Of those 89, 87 compile at LeanEval pins and 2 expose genuine 4.27→4.33 incompatibilities (Erdos1092.f_asymptotic_general, Irrational.irrational_e_to_e). The run also found a guillemet/dotted-module path decoder bug and an unqualified conjecture workspace-ID collision. Exact evidence and the failure list are posted at google-deepmind/formal-conjectures#4951 (comment). No import should proceed until the FC-owned adapter fixes these and a corrected frozen set passes the whole-set job.

[kim-em]

FC100 dependency audit is now reproduced at Formal Conjectures PR head a101a9c…: 100/100 declarations resolved; 280 closure edges, 158 unique FC constants in 74 modules, 56 generated auxiliaries; zero target-to-target dependencies. One structural failure remains, Erdos324.erdos_324.match_1 with no copied ancestor, so the adapter correctly fails closed. Full evidence: google-deepmind/formal-conjectures#4951 (comment). This closes the audit-reproduction task but does not unblock import.

[Paul-Lez]

Concerning the presence of (now) solved problems in FC100OpenSet1, I've commented on this here google-deepmind/formal-conjectures#5075.

[williamjblair]

Update: the FC-side gates are now green on formal-conjectures#4951 — 100/100 verified at FC pins, 97/100 compiled at LeanEval target pins, the three exceptions recorded and matching exactly (whole-set audit runs in FC CI; artifact on the PR). Two exceptions are pin-set Mathlib drift that FC's 4.33 bump retires.

Two items are remaining (also mentioned in PR)

1. Generator gap: the Challenge reconstruction re-extracts a local notation without the set_option quotPrecheck false it needs (repro: Erdos125.erdos_125.variants.positive_unequal_density). This will require a fix in lean-eval-generator with a regression fixture.
2. v1 has no provenance fields: the FC source commit and declaration id §10 requires currently travel as an fc-provenance.json sidecar — is a passthrough/provenance object in v2 preferred, or is the sidecar the intended shape?