Paper Citation Record · LEDGER

LEGO-Prover: Neural Theorem Proving with Growing Libraries

As of 9 August 2026, this Paper Citation Record lists 0 of 0 outbound references and 19 inbound Pith citation observations for arXiv:2310.00656.

A citation records a reference. It does not transfer a finding from one paper to another.

pith.paper-citation-record.v1
2310.00656 v3

Coverage vector

measured 0 of 0 reference resolution

Typed states for the displayed outbound observations.

Source: paper_references, paper_reference_links

measured 19 of 19 standing notices

One-hop event checks from named stored sources.

Source: scholarly_work_events, retraction_status_cache, observed 2026-08-09T06:31:02.800959+00:00

measured 19 of 19 inbound itemization

Pith citing papers itemized under the disclosed page cap.

Source: paper_references, paper_reference_links, observed 2026-08-09T05:12:15.745314Z

measured 0 of 1 external citation measurements

A source-named dated measurement, never combined with another source.

Source: arxiv_reference, observed 2026-07-04T19:10:04.276956Z

Reference resolution

0 of 0 outbound references displayed

verified exact0
verified fuzzy0
unresolved0
parse uncertain0
malformed identifier0
metadata mismatch0

External citation measurements

No source-named external measurement is stored.

Outbound references

No outbound reference observations are available for this paper version.

Pith citing papers

Observation bb219c47-ced0-458e-b51f-9fb8fb5bbcd7 · inbound

Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques cites this paper.

Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 27

Resolution: unresolved; no resolver link, observed 2026-08-09T05:12:15.745314Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation e2ed5352-a667-4e0d-bdb7-bada423db203 · inbound

Proving the Coding Interview: A Benchmark for Formally Verified Code Generation cites this paper.

Proving the Coding Interview: A Benchmark for Formally Verified Code Generation LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 7

Resolution: unresolved; no resolver link, observed 2026-08-08T18:20:22.519772Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation c2fc0635-efa5-402a-9fa1-f88516b75ac9 · inbound

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning cites this paper.

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 2

Resolution: verified exact; arxiv_id, observed 2026-05-17T18:32:40.918717Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-09T06:31:02.800959+00:00.

Observation 9f7fd8dc-95c5-4603-a7d4-e096737629b6 · inbound

Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine cites this paper.

Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 33

Resolution: unresolved; no resolver link, observed 2026-08-07T11:26:31.151825Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation d2058df4-a660-4a3f-874a-272d5e29756d · inbound

Mathesis: Towards Formal Theorem Proving from Natural Languages cites this paper.

Mathesis: Towards Formal Theorem Proving from Natural Languages LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 21

Resolution: unresolved; no resolver link, observed 2026-08-07T05:50:37.582568Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation 7d5b99e8-5c14-4a34-bdd8-4a0f4264ef87 · inbound

StepProof: Step-by-step verification of natural language mathematical proofs cites this paper.

StepProof: Step-by-step verification of natural language mathematical proofs LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 33

Resolution: unresolved; no resolver link, observed 2026-08-07T04:29:43.837522Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation d408067e-135e-41c7-9d7c-b2fd1bf069a3 · inbound

Clarifying Before Reasoning: A Coq Prover with Structural Context cites this paper.

Clarifying Before Reasoning: A Coq Prover with Structural Context LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 29

Resolution: unresolved; no resolver link, observed 2026-08-06T20:31:27.281171Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation 59aabeec-9984-4644-bd0c-aa2c767f5103 · inbound

Solving Formal Math Problems by Decomposition and Iterative Reflection cites this paper.

Solving Formal Math Problems by Decomposition and Iterative Reflection LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 38

Resolution: unresolved; no resolver link, observed 2026-08-06T15:42:08.504816Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation 36feea82-9a2a-409e-ab89-5cc73df27e9c · inbound

StepFun-Prover Preview: Let's Think and Verify Step by Step cites this paper.

StepFun-Prover Preview: Let's Think and Verify Step by Step LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 27

Resolution: unresolved; no resolver link, observed 2026-08-06T13:47:37.576970Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation 8400ccbe-1fcc-49be-b869-eb5c4140f682 · inbound

A Survey of Self-Evolving Agents: What, When, How, and Where to Evolve on the Path to Artificial Super Intelligence cites this paper.

A Survey of Self-Evolving Agents: What, When, How, and Where to Evolve on the Path to Artificial Super Intelligence LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 33

Resolution: verified exact; arxiv_id, observed 2026-05-14T22:23:15.547500Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-09T06:31:02.800959+00:00.

Observation 32f94fc4-ff56-47f3-a992-a178bf87fd54 · inbound

A Compute-Matched Re-Evaluation of TroVE on MATH cites this paper.

A Compute-Matched Re-Evaluation of TroVE on MATH LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 19

Resolution: unresolved; no resolver link, observed 2026-08-06T17:05:19.239606Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation 0878dc47-7271-48d2-a42a-aed0f743485e · inbound

Rethinking Wireless Communications through Formal Mathematical AI Reasoning cites this paper.

Rethinking Wireless Communications through Formal Mathematical AI Reasoning LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 68

Resolution: metadata mismatch; arxiv_id, observed 2026-05-12T00:11:16.348279Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-09T06:31:02.800959+00:00.

Observation 76baa175-1c68-4611-aed5-2b056f264ed7 · inbound

LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation cites this paper.

LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 22

Resolution: verified exact; arxiv_id, observed 2026-05-11T16:51:09.534736Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-09T06:31:02.800959+00:00.

Observation 244b7b1f-3aa0-42a3-b10c-6a6db7125321 · inbound

Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin cites this paper.

Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 41

Resolution: verified exact; arxiv_id, observed 2026-05-25T04:10:19.430662Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-09T06:31:02.800959+00:00.

Observation b68ba112-7551-4f56-974f-13ae1ba71011 · inbound

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4 cites this paper.

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4 LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 2

Resolution: verified exact; arxiv_id, observed 2026-06-29T19:53:55.464207Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-09T06:31:02.800959+00:00.

Observation 9d07a26d-1857-40ba-99ef-d39bec3ec1bb · inbound

Formalizing Mathematics at Scale cites this paper.

Formalizing Mathematics at Scale LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 47

Resolution: metadata mismatch; arxiv_id, observed 2026-06-29T07:53:14.288299Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-09T06:31:02.800959+00:00.

Observation 37be89b3-700b-4ef8-95d9-16beca363e81 · inbound

IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus cites this paper.

IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 62

Resolution: verified exact; arxiv_id, observed 2026-07-03T20:38:55.790303Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-09T06:31:02.800959+00:00.

Observation 5d7848b9-bb7e-4e9e-beb7-a9016c19b693 · inbound

Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language cites this paper.

Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 26

Resolution: verified exact; arxiv_id, observed 2026-07-04T19:10:04.279008Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-09T06:31:02.800959+00:00.

Observation 9dc78a3f-9a8b-471d-adc8-3f6a8a5a3206 · inbound

Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases cites this paper.

Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases LEGO-Prover: Neural Theorem Proving with Growing Libraries

Reference 34

Resolution: unresolved; no resolver link, observed 2026-08-02T05:40:00.998283Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.