vf_d190b51c42af9300 · Vela Observatory

Canonical assertion

The Formal Conjectures statement for Erdős problem 31 (FormalConjectures/ErdosProblems/31.lean, PR #4345) faithfully represents the informal problem.

Rendered from stored source; the pinned checkout remains the exact record.

Sourceexpert_assertion
Assertiontheoretical
Evidence0 spans
Reviewnot recorded
Standingrecorded

Scope and conditions

theoretical

Statement pinned at google-deepmind/formal-conjectures@8fd558fc8f3c76a5bd1972c10649ba320006d302 (sha256 310e092f8b6a9810ba28e4ceeb6b5ce348be56b217df8ea7ed6785a9b2765155); PR #4345 (open PR, statement subject to change until merge). Drafted pre-pipeline (batch-2b); gate evidence is the FC CI build on that commit. Requires fidelity review.

Source record

0 evidence spans

Source: formal-conjectures PR #4345
Type: expert_assertion
Recorded: Jul 2, 2026, 2:40 PM
Updated: not recorded

Reproduce the source snapshot

Replay establishes the exact record and checks. It does not add scientific authority.

Open reproduction

Exact record identityFinding ID, frontier identity, and pinned Git source

Finding ID: vf_d190b51c42af9300
Frontier: vfr_0a25edabc16db143
Commit: ce8ba7d934c848408e0d91caca39e938698e3fc7
Tree: 03f7371b496485f761f91961027fd48198dc7e93

Exact source and rootsGit ce8ba7d934c8 and content-addressed ledgers

Source identity

Commit: ce8ba7d934c848408e0d91caca39e938698e3fc7
Tree: 03f7371b496485f761f91961027fd48198dc7e93
Committed: 2026-07-20T19:20:20-04:00
Repository: Open source

Content roots

Event log: sha256:a06797bc0d1b0e3c88a2f97507fe0832661e3992d8df41187a0aa6d3ceee9bde
Snapshot: sha256:1faedc24f040a60a22177b456c74b969a61ce8836082297b1835797a57b4fa56
Proposals: sha256:e69b38037814f2e8ca826942cfc50ab370993889be2913cac1c0b3e77711160f
Actor registry: sha256:665f3e1c48f0a50fac949681c0af01bdd28de2991f2cdc5cc4cddbe69df6311b
Artifacts: sha256:3d58619c5cfb7e28de2f344476e35c9f0b80709c996b2a1bfdb2e11496f7e1da