erdos-frontier-atlas

KO | EN

gitlite — search

#windows #tensorflow #open-source #bash #security #ai-agent #mcp #mysql #cross-platform #ruby

erdos-frontier-atlas

(★ 9)

Machine-readable map of the computational frontier around Erdős prize problems: 95 audited (17 board-ready), walls named, verifier-first P42 board specs. No Erdős prize is claimable by finite computation — this maps what IS.

File Explorer

ZIP Download

- - verify.yml
- - graph.json
  - quarantine.json
- - computed_statuses.json
  - crater.json
  - geometric_degree.py
  - implication_graph.json
  - map_degree.py
  - padding_check.py
  - quantities.json
  - README.md
  - root_claim.json
- ai_claims.json
- effectivization_shortlist.json
- finite_handle_triage.json
- gap_map.json
- gap_map.schema.json
- lanes.md
- lean_lane.json
- problems.json
- schema.json
- stub.schema.json
- stubs.json
- substrate.json
- walls.md
- - 00-preface.md
  - 01-the-map.md
  - 02-fences.md
  - 03-the-observatory.md
  - 04-walls.md
  - 05-methods.md
- BOOK.md
- build_book.py
- - README.md
  - SOURCES.md
  - weyl_endomorphism.py
- - README.md
  - verify.py
- - README.md
  - table.json
  - verify.py
- - _verify_affine.py
  - _verify_enum.py
  - affine_farkas_cert.json
  - enumeration_certificate.json
  - fulldim_cells.json
  - geometry.json
  - README.md
  - verify.py
- - README.md
  - verify.py
  - witnesses.json
- - README.md
  - verify.py
  - witnesses.json
- - constants.json
  - README.md
  - verify.py
- - .gitignore
  - emit_result.py
  - README.md
  - reference.py
  - RESULT.json
  - run_sweep.sh
  - search366.c
  - verify.py
- - README.md
  - verify.py
  - witnesses.json
- - README.md
  - verify.py
  - witness.json
- - build_cnf.py
  - FINDINGS.md
- - emit_result.py
  - exact.py
  - FINDINGS.md
  - README.md
  - reference.py
  - RESULT.json
  - run699.sh
  - verify.py
- - .gitignore
  - emit_result.py
  - gen_trees.py
  - pack.c
  - README.md
  - RESULT.json
  - run743.sh
  - trees.txt
  - verify.py
- - RECEIPT.md
  - verify.py
- - .gitignore
  - emit_result.py
  - freetrees.py
  - README.md
  - RESULT.json
  - run993.sh
  - unimodal.c
  - verify.py
- - exhaust_n7_n6boost.py
  - gen_verifier.py
  - hunt_n_fast.py
  - hunt_n_from_prev.py
  - INDUCTION_NOTES_L3.md
  - macro_engine.py
  - mine_n7.py
  - MORPHOGENESIS.md
  - N10_HUNT.json
  - N10_L6_S7_MACRO_WITNESS_RESULT.json
  - N10_L6_S7_WITNESS.json
  - N10_L8_S7_MACRO_WITNESS_RESULT.json
  - N10_L8_S7_WITNESS.json
  - N11_HUNT.json
  - N11_L7_S7_MACRO_WITNESS_RESULT.json
  - N11_L7_S7_WITNESS.json
  - N12_HUNT.json
  - N12_L8_S8_MACRO_WITNESS_RESULT.json
  - N12_L8_S8_WITNESS.json
  - N13_HUNT.json
  - N13_L9_S9_MACRO_WITNESS_RESULT.json
  - N13_L9_S9_WITNESS.json
  - N14_HUNT.json
  - N3_L3_MACRO_WITNESS_RESULT.json
  - N4_L3_MACRO_WITNESS_RESULT.json
  - N4_L3_WITNESS.json
  - N5_L3_S3_COMPLETE.json
  - N5_L3_S4_COMPLETE.json
  - N5_L3_S4_INTEGER_PROGRESS.json
  - N5_L3_S4_INTEGER_SEARCH.json
  - N5_L3_S4_MACRO_WITNESS_RESULT.json
  - N5_L3_S4_PROGRESS.json
  - N5_L3_S4_SAMPLE.json
  - N5_L3_S4_WITNESS.json
  - N5_L3_S4_WITNESS_RESULT.json
  - N5_L4_S3_COMPLETE.json
  - N5_L5_S3_COMPLETE.json
  - N6_L3_S3_COMPLETE.json
  - N6_L3_S3_SMOKE.json
  - N6_L3_S4_FIRST_ROUTABLE.json
  - N6_L3_S4_PROGRESS.json
  - N6_L3_S4_SEARCH.json
  - N6_L3_S4_SMOKE.json
  - N6_L3_S5_CLOCK0_EXHAUST.json
  - N6_L3_S5_FIRST_ROUTABLE.json
  - N6_L3_S5_INTEGER_PROGRESS.json
  - N6_L3_S5_INTEGER_SEARCH.json
  - N6_L3_S5_SAMPLE.json
  - N6_L3_S5_SEED_HUNT.json
  - N6_L4_S3_COMPLETE.json
  - N6_L4_S5_MACRO_WITNESS_RESULT.json
  - N6_L4_S5_SAMPLE.json
  - N6_L4_S5_WITNESS.json
  - N6_L5_S3_COMPLETE.json
  - N7_HUNT.json
  - N7_L3_S4_COMPLETE.json
  - N7_L5_S5_MACRO_WITNESS_RESULT.json
  - N7_L5_S5_WITNESS.json
  - N7_L5_S6_MACRO_WITNESS_RESULT.json
  - N7_L5_S6_WITNESS.json
  - N7_SEARCH.json
  - N8_HUNT.json
  - N8_L3_S4_COMPLETE.json
  - N8_L6_S6_MACRO_WITNESS_RESULT.json
  - N8_L6_S6_WITNESS.json
  - N9_HUNT.json
  - N9_L6_S6_MACRO_WITNESS_RESULT.json
  - N9_L6_S6_WITNESS.json
  - N9_L7_S7_HUNT.json
  - N9_L7_S7_MACRO_WITNESS_RESULT.json
  - N9_L7_S7_WITNESS.json
  - PORT_CAPACITY_MULTI_S.json
  - PORT_CAPACITY_N7_GE8_SUMMARY.json
  - PORT_CAPACITY_S3.json
  - PORT_CAPACITY_S4.json
  - PORT_CAPACITY_S5_L4_SAMPLE.json
  - PORT_CAPACITY_S5_L5_SAMPLE.json
  - PORT_CAPACITY_S5_SAMPLE.json
  - PORT_CAPACITY_S6_L4_SAMPLE.json
  - PORT_CAPACITY_SAMPLE_HIGH.json
  - pure_lp.py
  - README.md
  - recover_n5_l3_s4_witness.py
  - route_enum.py
  - sample_n5_l3_s4_routability.py
  - sample_n6_l3_s5.py
  - SEAL.json
  - search_n5_l3.py
  - search_n5_l3_s3_complete.py
  - search_n5_l3_s4_integer.py
  - search_n6_l3_s4_routability.py
  - search_n6_l3_s5_integer.py
  - search_n6_s5_from_seeds.py
  - search_n7_from_n6.py
  - search_n8_smoke.py
  - search_n_l3_s4_by_ports.py
  - THEOREM_L3_S_LE_4_CLASSIFICATION.md
  - THEOREM_N10_L6_S7_SPLIT_MACRO_WITNESS.md
  - THEOREM_N11_L7_S7_SPLIT_MACRO_WITNESS.md
  - THEOREM_N12_L8_S8_SPLIT_MACRO_WITNESS.md
  - THEOREM_N13_L9_S9_SPLIT_MACRO_WITNESS.md
  - THEOREM_N3_L2_ALL_S_NO_GO.md
  - THEOREM_N3_L3_SPLIT_MACRO_WITNESS.md
  - THEOREM_N4_L3_SPLIT_MACRO_WITNESS.md
  - THEOREM_N5_L3_S3_NO_GO.md
  - THEOREM_N5_L3_S4_ROUTABLE.md
  - THEOREM_N5_L3_S4_SPLIT_MACRO_WITNESS.md
  - THEOREM_N5_L4_S3_NO_GO.md
  - THEOREM_N5_L5_S3_NO_GO.md
  - THEOREM_N6_L3_S3_NO_GO.md
  - THEOREM_N6_L3_S4_NO_GO.md
  - THEOREM_N6_L3_S5_LP_FENCE.md
  - THEOREM_N6_L4_S5_SPLIT_MACRO_WITNESS.md
  - THEOREM_N7_L3_S4_NO_GO.md
  - THEOREM_N7_L4_SAMPLE_FENCES.md
  - THEOREM_N7_L5_S5_SPLIT_MACRO_WITNESS.md
  - THEOREM_N7_LOWER_BOUNDS.md
  - THEOREM_N8_L3_S4_NO_GO.md
  - THEOREM_N8_L6_S6_SPLIT_MACRO_WITNESS.md
  - THEOREM_N9_L6_S6_SPLIT_MACRO_WITNESS.md
  - THEOREM_N9_L7_S7_SPLIT_MACRO_WITNESS.md
  - THEOREM_N_GE_7_S3_PORT_CAPACITY.md
  - THEOREM_S4_PORT_CAPACITY.md
  - tool_n7_macro_witness.py
  - verify_n10_l6_s7_macro_witness.py
  - verify_n10_l8_s7_macro_witness.py
  - verify_n11_l7_s7_macro_witness.py
  - verify_n12_l8_s8_macro_witness.py
  - verify_n13_l9_s9_macro_witness.py
  - verify_n3_l3_macro_witness.py
  - verify_n4_l3_macro_witness.py
  - verify_n5_l3_s3_routability.py
  - verify_n5_l3_s4_macro_witness.py
  - verify_n5_l3_s4_routability.py
  - verify_n5_l4_s3_routability.py
  - verify_n6_l3_s3_routability.py
  - verify_n6_l4_s5_macro_witness.py
  - verify_n7_l5_s5_macro_witness.py
  - verify_n7_l5_s6_macro_witness.py
  - verify_n8_l6_s6_macro_witness.py
  - verify_n9_l6_s6_macro_witness.py
  - verify_n9_l7_s7_macro_witness.py
  - verify_s3_port_capacity.py
  - verify_s4_port_capacity.py
- - README.md
  - table.json
  - verify.py
- - README.md
  - receipt.json
  - verify.py
- - .gitignore
  - certificate.json
  - README.md
  - verify.py
- - README.md
  - verify.py
  - witness.json
- - certify_nonproperness.py
  - cusp_curve_empty.py
  - degree_floor_check.py
  - fiber_anchors.py
  - fiber_count_generic.py
  - findings_fibers.md
  - findings_nonproperness.md
  - galois_group_s3.py
  - README.md
  - run_all.sh
- - CONST_JAC_K12_BOX.json
  - CONST_JAC_K2.json
  - CONST_JAC_K3_NEAR.json
  - FIBER_OFF_VE_CONTROL.json
  - FIBER_PARAM_DENSE.json
  - FIBER_Q0_SLICE.json
  - FIBER_SIZE2_EXACT.json
  - FIBER_SIZE2_EXACT_V2.json
  - FIBER_SIZE2_SHAPE.json
  - FIBER_T2_ZERO.json
  - FIBER_TWO_Y_CONJECTURE.json
  - GRADIENT_SPARSE.json
  - probe_const_jac_family.py
  - probe_const_jac_k3_near.py
  - probe_druzkowski_dim3.py
  - probe_fiber_param_slice.py
  - probe_fiber_q0_slice.py
  - probe_fiber_size2_disc.py
  - probe_fiber_size2_exact.py
  - probe_fiber_t2_zero.py
  - README.md
  - search_degree_family.py
  - THEOREM_DEGREE_FAMILY_PROBE.md
  - THEOREM_FIBER_SPECTRUM_PROBE.md
  - THEOREM_FIBER_TWO_Y_SOFT.md
- - README.md
  - verify.py
  - witness.json
- - BCW_FORMAL.json
  - bcw_formal_inverse.py
  - CRACK_AXIS_DEGFREE.json
  - crack_axis_degfree.py
  - CRACK_AXIS_INDUCTION.json
  - crack_axis_induction.py
  - CRACK_DEG3.json
  - crack_deg3_elim.py
  - crack_deg3_fullclass.py
  - CRACK_DEG4.json
  - crack_deg4.py
  - CRACK_DEGX1_FULL.json
  - crack_degx1_full.py
  - CRACK_EXOTIC.json
  - crack_exotic_obstruction.py
  - crack_full_plane.py
  - CRACK_G1_COMPLETE.json
  - crack_G1_complete.py
  - CRACK_G1_FREE.json
  - crack_G1_free.py
  - CRACK_G1_PUREPOWER.json
  - crack_G1_purepower.py
  - CRACK_GEODEG.json
  - crack_geodeg.py
  - CRACK_INDUCTION.json
  - crack_induction.py
  - CRACK_INVERSE_BOUND.json
  - crack_inverse_bound.py
  - CRACK_MULTIMIXED.json
  - crack_multimixed.py
  - CRACK_PLANE_CORE.json
  - crack_plane_core.py
  - CRACK_PLANE_JC_FULL.json
  - crack_plane_jc_full.py
  - CRACK_POISSON_HANKEL.json
  - crack_poisson_hankel.py
  - CRACK_PUREPOWER.json
  - crack_purepower.py
  - CRACK_STRUCTURAL.json
  - crack_structural.py
  - CRACK_TAME.json
  - crack_tame_classify.py
  - crack_triangularize.py
  - CRACK_XDEGREE.json
  - crack_xdegree.py
  - CRACK_XDROP_FULL.json
  - crack_xdrop_full.py
  - PACK_REPLAY.json
  - pack_replay.py
  - PERETZ_RESULTANT.json
  - peretz_resultant.py
  - PLANE_PROPERNESS.json
  - plane_properness.py
  - plane_quantities.json
  - poly2.py
  - README.md
  - RESOLUTION.md
  - tame_invert.py
  - THEOREM_CRACK_DEG3.md
  - THEOREM_PLANE_JC.md
  - THEOREM_PLANE_JC_CORE.md
  - THEOREM_PLANE_JC_DEG3_SEALED.md
  - THEOREM_PLANE_JC_REDUCTION.md
  - wang_degree2.py
  - YU_NONNEGATIVE.json
  - yu_nonnegative.py
- - problem.cnf
  - proof.drat
  - README.md
  - truncated_negctl.drat
- - problem.cnf
  - proof.drat
  - README.md
  - truncated_negctl.drat
- - METHOD.md
- - README.md
  - verify.py
- contracts.json
- README.md
- - 699-audit-result.json
  - 699-independent-audit.md
  - 699-strip.md
  - 993-block-result.json
  - 993-block.md
  - audit_699_receipt.py
  - check_699_lemmas.py
  - check_993_block.py
  - code-review.json
  - freshness.md
  - hubpath-random-summary.json
  - lemma-checks.json
  - MANIFEST.json
  - manuscript-pin.json
  - mutation-results.json
  - probe.py
  - README.md
  - RESULT.json
  - sources.json
  - test_probe.py
  - threehub-random-batch1.json
  - topology-control.json
  - upstream-diff.json
  - verification.json
- - citations.json
  - execution.json
  - fiber.py
  - FRESHNESS.md
  - README.md
  - receipt.json
  - RESULT.md
  - review.json
  - sources.json
  - test_fiber.py
  - test_receipt.py
  - verify.py
- - .gitignore
  - hits-d35.txt
  - kummer105.py
  - README.md
  - search.md
  - search_base3.c
  - test_kummer.py
  - test_search.py
- - briefcase.html
  - briefcase.template.html
  - MANIFEST.json
  - million-vertex-tail.json
  - README.md
  - tail.py
  - test_block_cli.py
  - test_block_tables.py
  - test_bridge_receipt.py
  - test_tail.py
  - transfer-audit.md
  - transfer-h3.json
  - transfer-h4.json
  - transfer-h5.json
  - transfer-h6.json
  - transfer-h7.json
  - transfer-h8.json
  - transfer-summary.json
  - transfer-theorem.md
  - verify.py
- - README.md
  - upstream-diff.json
- - .gitignore
  - AxiomAudit.lean
  - ExactStatement.lean
  - execution.json
  - I2All.lean
  - i2all.py
  - README.md
  - result.md
  - test_i2all.py
  - verify.py
- - .gitignore
  - AxiomAudit.lean
  - ExactStatement.lean
  - execution.json
  - i2.py
  - MANIFEST.json
  - official-delta.json
  - P699I2.lean
  - README.md
  - test_i2.py
  - verify.py
- - .gitignore
  - AxiomAudit.lean
  - bands.md
  - bands.py
  - close.md
  - ExactStatement.lean
  - execution.json
  - GOAL.md
  - I3.lean
  - i3.py
  - mod4.md
  - mod4.py
  - README.md
  - residual.md
  - residual.py
  - result.md
  - STACK.md
  - test_bands.py
  - test_close.py
  - test_i3.py
  - test_mod4.py
  - test_residual.py
  - test_typeA.py
  - test_typeB1.py
  - test_typeB2a.py
  - test_typeB2b.py
  - typeA.md
  - typeA.py
  - typeB1.md
  - typeB1.py
  - typeB2a.md
  - typeB2a.py
  - typeB2b.md
  - typeB2b.py
  - verify.py
- - .gitignore
  - AdjacentBinomialGcd.lean
  - AxiomAudit.lean
  - DivisorTransferCheck.lean
  - ExactStatement.lean
  - execution.json
  - lake-manifest.json
  - lakefile.toml
  - lean-toolchain
  - LibraryChecks.lean
  - MANIFEST.json
  - proof-obligations.json
  - README.md
- - ANALYTIC_TARGET.md
  - citations.json
  - execution.json
  - floor_transfer.py
  - FRESHNESS.md
  - LIVE_CODE_REVIEW.json
  - LIVE_CODE_REVIEW_INTAKE.json
  - PARSER_FIX_VERIFICATION.json
  - README.md
  - receipt.json
  - repository-verification-final.json
  - repository-verification-hardened.json
  - repository-verification-publication.json
  - repository-verification.json
  - REPOSITORY_STATUS.md
  - RESULT.md
  - review.json
  - SOFTWARE_REVIEW.json
  - test_floor.py
  - test_persistence.py
  - test_receipt.py
  - verify.py
- - ARCHIVE_CODE_REVIEW.json
  - ARCHIVE_CODE_REVIEW_INTAKE.json
  - ARITHMETIC_FRONTIER.md
  - audit-preservation-verification.json
  - citations.json
  - code_review.json
  - diagonal_review.json
  - execution.json
  - gm_parameter_check.json
  - GM_TRANSFER.md
  - HARNESS_MAINTENANCE.json
  - HARNESS_MAINTENANCE_INITIAL.json
  - kernel.py
  - mellin_arithmetic.json
  - MELLIN_TRANSFER.md
  - portability.json
  - README.md
  - receipt.json
  - RESULT.md
  - REVIEW_STATUS.json
  - test_kernel.py
  - test_receipt.py
  - typeI_review.json
  - verify.py
- - BOARD.md
  - README.md
  - verify.py
- measurements.json
- pipeline.json
- README.md
- - 20260715_cross_frontier_global_gate.json
  - 20260715_stretched_lr_quantity_conflation.json
- index.json
- README.md
- schema.json
- hello_frontier.sh
- test_ai_claims.py
- test_book.py
- test_certificate_contracts.py
- test_certificate_replay.py
- test_ci_workflow_is_runnable.py
- test_crater_engine.py
- test_doc_links.py
- test_emit_check_split.py
- test_finite_handle_preserved.py
- test_finite_handle_triage.py
- test_gap_map.py
- test_gen_r3k_cnf.py
- test_graph.py
- test_jc_crater.py
- test_no_private_infrastructure.py
- test_p327_fiber.py
- test_readme.py
- test_rh969.py
- test_rh_audit_archive.py
- test_rh_crt.py
- test_state_of_frontier.py
- test_stubs.py
- test_substrate.py
- test_walled_finite_handles_are_explained.py
- - __init__.py
  - checks.py
  - driver.py
  - engine.py
  - render.py
  - scaffold.py
  - schema.py
  - selftest.py
  - spec.py
- atlas2p42.py
- build_graph.py
- build_problems.py
- build_stubs.py
- check_certificate_contracts.py
- check_receipt_drift.py
- crater.py
- gen_r3k_cnf.py
- jc_root_tripwire.py
- query_graph.py
- query_substrate.py
- state_of_frontier.py
- validate_ai_claims.py
- validate_atlas.py
- validate_crater.py
- validate_gap_map.py
- validate_graph.py
- validate_jc_crater.py
- - INDEX.md
  - P1.md
  - P10.md
  - P1003.md
  - P1005.md
  - P101.md
  - P1013.md
  - P1016.md
  - P1020.md
  - P1029.md
  - P1030.md
  - P1032.md
  - P1033.md
  - P1038.md
  - P1039.md
  - P104.md
  - P1040.md
  - P1041.md
  - P1052.md
  - P1053.md
  - P1054.md
  - P1055.md
  - P1056.md
  - P1057.md
  - P1059.md
  - P106.md
  - P1060.md
  - P1061.md
  - P1062.md
  - P1063.md
  - P107.md
  - P1073.md
  - P1082.md
  - P1083.md
  - P1084.md
  - P1085.md
  - P1095.md
  - P11.md
  - P1100.md
  - P1101.md
  - P1103.md
  - P1104.md
  - P1106.md
  - P1107.md
  - P1108.md
  - P1109.md
  - P1113.md
  - P1135.md
  - P1137.md
  - P114.md
  - P1142.md
  - P1160.md
  - P12.md
  - P1204.md
  - P1208.md
  - P124.md
  - P128.md
  - P13.md
  - P131.md
  - P138.md
  - P139.md
  - P14.md
  - P140.md
  - P141.md
  - P142.md
  - P145.md
  - P146.md
  - P148.md
  - P155.md
  - P156.md
  - P159.md
  - P161.md
  - P165.md
  - P166.md
  - P167.md
  - P168.md
  - P169.md
  - P17.md
  - P170.md
  - P171.md
  - P176.md
  - P18.md
  - P182.md
  - P183.md
  - P185.md
  - P19.md
  - P193.md
  - P2.md
  - P20.md
  - P200.md
  - P201.md
  - P208.md
  - P21.md
  - P211.md
  - P218.md
  - P222.md
  - P23.md
  - P233.md
  - P236.md
  - P241.md
  - P242.md
  - P243.md
  - P249.md
  - P251.md
  - P252.md
  - P27.md
  - P271.md
  - P287.md
  - P291.md
  - P295.md
  - P3.md
  - P30.md
  - P301.md
  - P302.md
  - P304.md
  - P306.md
  - P307.md
  - P313.md
  - P322.md
  - P327.md
  - P334.md
  - P340.md
  - P342.md
  - P345.md
  - P357.md
  - P359.md
  - P36.md
  - P364.md
  - P365.md
  - P366.md
  - P367.md
  - P368.md
  - P371.md
  - P373.md
  - P374.md
  - P375.md
  - P376.md
  - P382.md
  - P385.md
  - P386.md
  - P389.md
  - P39.md
  - P390.md
  - P393.md
  - P394.md
  - P396.md
  - P398.md
  - P408.md
  - P409.md
  - P41.md
  - P410.md
  - P411.md
  - P412.md
  - P413.md
  - P416.md
  - P417.md
  - P421.md
  - P422.md
  - P423.md
  - P424.md
  - P43.md
  - P436.md
  - P451.md
  - P454.md
  - P456.md
  - P458.md
  - P462.md
  - P468.md
  - P469.md
  - P470.md
  - P472.md
  - P475.md
  - P477.md
  - P478.md
  - P479.md
  - P483.md
  - P488.md
  - P5.md
  - P500.md
  - P501.md
  - P503.md
  - P506.md
  - P51.md
  - P52.md
  - P524.md
  - P528.md
  - P530.md
  - P539.md
  - P544.md
  - P545.md
  - P547.md
  - P548.md
  - P551.md
  - P552.md
  - P555.md
  - P556.md
  - P564.md
  - P573.md
  - P580.md
  - P582.md
  - P583.md
  - P588.md
  - P60.md
  - P617.md
  - P628.md
  - P64.md
  - P647.md
  - P654.md
  - P663.md
  - P668.md
  - P669.md
  - P67.md
  - P672.md
  - P676.md
  - P68.md
  - P681.md
  - P683.md
  - P684.md
  - P687.md
  - P693.md
  - P695.md
  - P699.md
  - P7.md
  - P700.md
  - P703.md
  - P707.md
  - P708.md
  - P710.md
  - P712.md
  - P720.md
  - P723.md
  - P724.md
  - P725.md
  - P727.md
  - P730.md
  - P731.md
  - P742.md
  - P743.md
  - P768.md
  - P769.md
  - P77.md
  - P770.md
  - P773.md
  - P779.md
  - P78.md
  - P786.md
  - P791.md
  - P812.md
  - P82.md
  - P820.md
  - P821.md
  - P83.md
  - P830.md
  - P835.md
  - P848.md
  - P849.md
  - P85.md
  - P852.md
  - P853.md
  - P854.md
  - P855.md
  - P86.md
  - P860.md
  - P864.md
  - P87.md
  - P878.md
  - P879.md
  - P89.md
  - P893.md
  - P9.md
  - P90.md
  - P902.md
  - P91.md
  - P912.md
  - P913.md
  - P92.md
  - P928.md
  - P932.md
  - P935.md
  - P936.md
  - P938.md
  - P942.md
  - P945.md
  - P954.md
  - P961.md
  - P962.md
  - P968.md
  - P969.md
  - P97.md
  - P970.md
  - P971.md
  - P975.md
  - P979.md
  - P982.md
  - P985.md
  - P993.md
- board_catalog.md
- index.md
- operations.md
- sorties.md
- state_of_frontier.md
.gitignore
.zenodo.json
CITATION.cff
CLAUDE.md
COORDINATION.md
FRONTIER_CARTOGRAPHY.md
GRAPH.md
LICENSE
Makefile
NOTICE
README.md
RELEASING.md
requirements-dev.lock

# Use via CDN

jsDelivr

jsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.

Version

File

Link

Example

# Project Badges

DOI Visit

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

**A method substrate and strike map for mathematical research.**

The Atlas connects Erdős problems to reusable lemmas, explicit remaining
obligations, source records, and evidence another researcher can check. A useful
result can be a proof transfer, a conditional reduction, or a failed route that
saves the next person from repeating it. Larger computational cutoffs are useful
only when they answer a worthwhile mathematical question.

The production attack graph and published certificates are preserved separately
from active research. Adding a method does not change a problem's status, prove a
conjecture, or turn a shared tag into an implication. The
[campaign goal](experiments/astra-i3-20260911/GOAL.md) explains this direction;
[frontier cartography](FRONTIER_CARTOGRAPHY.md) is the broader charter.

## Start here

| To… | Read or run |
|---|---|
| Find a reusable method | [Method substrate](experiments/astra-substrate-20260911/README.md) · [generated method board](experiments/astra-substrate-20260911/BOARD.md) |
| Read the RH / squarefree-counting work | [P969 progress map](experiments/astra-rh-969-20260912/REPOSITORY_STATUS.md), including derivations, audit evidence, verification and remaining obligations |
| Choose a research direction | [Agent entry point](GRAPH.md) · [strike board](views/sorties.md) · [walls](atlas/walls.md), then check [source freshness](#source-freshness) |
| Inspect the dataset | [State of the Frontier](views/state_of_frontier.md) · [source ledgers](#repository-inventory) |
| Replay the work | [Quickstart and verification](#quickstart-and-verification) |
| Contribute without clobbering another lane | [Coordination](COORDINATION.md) · [contribution rules](#contributing--humans-and-agents) |
| Read the longer account | [*Cartography of Numbers*](book/BOOK.md) |

## Current research

These are research results and interfaces, not a list of solved conjectures.
The [method registry](atlas/substrate.json) records each statement's hypotheses,
artifacts, evidence level, and unresolved step.

| Lane | What is available | What remains open |
|---|---|---|
| **RH / P969** | [Squarefree-energy equivalence and generic obstruction](experiments/astra-rh-969-20260912/README.md); CRT/centered-defect and Mellin transfers; the [GM/GMRR assembled variance deduction](experiments/astra-rh-crt-20260912/GM_TRANSFER.md) through `4/7-epsilon`; [sharp Type I and signed-diagonal interfaces](experiments/astra-rh-crt-20260912/ARITHMETIC_FRONTIER.md) | The RH-equivalent energy estimate and full signed mixed-moment saving are unproved. The variance deduction uses pinned external theorems and model audits; it is not a novelty, record, human-review, or formal-proof claim. |
| **P327** | [Multiplier-sensitive smooth-fiber transfer](experiments/astra-327-fiber-20260912/README.md): retain multiplier divisibility information and prove an all-N deficit inequality, with a small independently checked demonstration | No solution or new best bound. The demonstration's bounds are weaker than the cited literature. Published for review in [PR #155](https://github.com/techno-optimist/erdos-frontier-atlas/pull/155). |
| **P699** | [Formal binomial-gcd seeds](experiments/astra-lean-seed-20260904/README.md), [the i=2 case](experiments/astra-i2-complete-20260911/README.md), and [i=3 reductions and residuals](experiments/astra-i3-20260911/GOAL.md) | Each formal or conditional lemma has its own scope. The remaining i=3 obligations and higher-i cases are not closed by these artifacts. |
| **P993 and CRT bridges** | [Tail compression, Laurent blocks and endpoint-safe transfers](experiments/astra-briefcase-20260904/README.md) | Block properties and candidate matches are not proofs of tree unimodality or an entire gap spectrum. |
| **P376** | [Kummer/digit checks and bounded historical replay](experiments/astra-376-20260911/README.md) | The infinitude question needs a method, not another extension of a known sequence's cutoff. The [working goal](experiments/astra-i3-20260911/GOAL.md) records that correction. |

The RH update is published for review in
[PR #156](https://github.com/techno-optimist/erdos-frontier-atlas/pull/156), stacked
on the P327 method PR. It does not solve P969 or RH. Its
[portable audit archive](experiments/astra-rh-crt-20260912/audits/README.md)
separates exact arithmetic from numerical diagnostics, model review from human
review, and replayed checkers from those needing excluded source files. The
[progress map](experiments/astra-rh-969-20260912/REPOSITORY_STATUS.md) carries the
integration record rather than a permanently hardcoded test total here.

To use the substrate from the repository root:

```sh
python3 tools/query_substrate.py methods
python3 tools/query_substrate.py for 969
python3 tools/query_substrate.py for 327
python3 tools/query_substrate.py for 699
python3 tools/query_substrate.py open
```

A `CANDIDATE` match is a search lead. A `discharges` entry applies only to the
stated lemma or obligation; it does not mean the parent conjecture is solved.
The substrate is an additive overlay, not a replacement for the production graph.

## Repository inventory

Counts below describe this checkout, not the current size of the upstream
website. `tests/test_readme.py` checks them against the source ledgers.

| Inventory | Count | Source of truth |
|---|---:|---|
| Hub records | 1,217 | [`atlas/stubs.json`](atlas/stubs.json), including its upstream commit pins |
| Deep-tier records | 51 | [`atlas/problems.json`](atlas/problems.json), with per-record provenance and scope |
| Bracketed quantities | 225 | [`atlas/gap_map.json`](atlas/gap_map.json); evidence determines the validator's C0–C3 class |
| Registered methods | 29 | [`atlas/substrate.json`](atlas/substrate.json); formal, informal, conditional and candidate scopes remain distinct |

The hub supplies problem identifiers and metadata. Deep records and bracketed
quantities describe selected evidence and computational questions. The method
registry adds transferable arguments and their remaining obligations. None of
these inventories is a count of conjectures solved by this project.

### The map — where everything lives

| Area | Files |
|---|---|
| Research methods | [`atlas/substrate.json`](atlas/substrate.json) · [`experiments/`](experiments) · [method board](experiments/astra-substrate-20260911/BOARD.md) |
| Production attack graph | [`GRAPH.md`](GRAPH.md) · [`atlas/graph/`](atlas/graph) · [`views/graph/`](views/graph) · [`views/sorties.md`](views/sorties.md) |
| Certificates and claim contracts | [`certificates/README.md`](certificates/README.md) · [`certificates/contracts.json`](certificates/contracts.json) |
| Feasibility and source overlays | [`atlas/walls.md`](atlas/walls.md) · [`atlas/lanes.md`](atlas/lanes.md) · [`atlas/ai_claims.json`](atlas/ai_claims.json) · [`atlas/lean_lane.json`](atlas/lean_lane.json) |
| Generated views and book | [`views/`](views) · [operations annex](views/operations.md) · [`book/`](book) |
| Validators and tests | [`tools/`](tools) · [`tests/`](tests) · [`Makefile`](Makefile) · [CI workflow](.github/workflows/verify.yml) |
| Project policy and releases | [`COORDINATION.md`](COORDINATION.md) · [`FRONTIER_CARTOGRAPHY.md`](FRONTIER_CARTOGRAPHY.md) · [`RELEASING.md`](RELEASING.md) · [`NOTICE`](NOTICE) |

## Source freshness

**The generated graph is a pinned snapshot, not a live upstream feed.** A passing
staleness gate means generated files agree with their source data; it does not
mean every source has been checked against today's literature. Some production
statuses are superseded by the dated research overlays, intentionally without
silently rebuilding the graph.

- The [September 11 Erdős update](experiments/astra-freshness-20260911/README.md)
  records the checked changes for #477, #625 and #501, distinguishes mathematical
  status changes from Lean-label changes, and preserves differences between the
  website and YAML snapshots.
- The [RH source review](experiments/astra-rh-969-20260912/FRESHNESS.md) and
  [P327 review](experiments/astra-327-fiber-20260912/FRESHNESS.md) are dated
  September 12, 2026. They are source snapshots, not continuing monitors.
- The [AI-claim overlay](atlas/ai_claims.json) is a dated claims registry.
  Recording an AI-assisted proof claim never changes a canonical status.
- Before starting a new attack, check the official problem page, discussion,
  separate proof-claim register, and cited manuscript versions. Consult
  [erdosproblems.com](https://www.erdosproblems.com) for the human-maintained
  index; do not infer current status from an old attack card or prize label.

The repository is a computational and research annex to that index, not a copy
of its prose. Machine metadata sources and licenses are recorded in
[`NOTICE`](NOTICE) and the source ledgers.

## Quickstart and verification

From the repository root, these bounded method replays use Python's standard
library:

```sh
python3 -I -B experiments/astra-substrate-20260911/verify.py
python3 -I -B experiments/astra-327-fiber-20260912/verify.py --negative-controls
python3 -I -B experiments/astra-rh-969-20260912/verify.py
python3 -I -B experiments/astra-rh-crt-20260912/verify.py experiments/astra-rh-crt-20260912/receipt.json
```

For the full fast repository gate with the pinned dependencies:

```sh
uv run --python 3.11 --with-requirements requirements-dev.lock make audit-fast
```

Without `uv`, use a virtual environment:

```sh
python3 -m venv .venv
. .venv/bin/activate
python -m pip install -r requirements-dev.lock
make audit-fast
```

`audit-fast` runs the atlas, gap-map and claim validators, checks generated views,
book and graph, verifies claim contracts, runs their fast replay profile, and
executes the repository tests. It does not recompile every Lean project, rerun
large historical searches, or recheck every cited analytic theorem.

The [CI workflow](.github/workflows/verify.yml) uses Python 3.12 for the fast gate.
Its slower receipt-drift job runs on the schedule or manual dispatch, not on
every PR. Run `make check-receipts` before merging certificate changes, following
the frozen-certificate policy; read its coverage report rather than interpreting
a pass as certification of every stored receipt. Slow claim replays have separate
resource requirements documented in the [Makefile](Makefile).

The [RH audit archive](experiments/astra-rh-crt-20260912/audits/README.md) has its
own scratch-only replay command and explicit source-dependent exclusions.
Default method verifiers read and recompute evidence without replacing it.
Emission commands are separate and require a new output path.

## Honest scope

- A finite exact check proves only the stated finite claim. An asymptotic theorem
  needs an argument covering its unbounded parameters.
- A formal theorem is checked relative to its declared dependencies and axioms.
  A passing Python gate does not establish a Lean rebuild or a human review.
- Model audits, human peer review, formal kernel checks and official acceptance
  are different kinds of evidence. None silently substitutes for another.
- A generic-coefficient countermodel is not a Möbius counterexample. An unsigned
  collision count is not a lower bound for a signed moment.
- A shared tag, OEIS sequence or graph neighbor suggests a question; only a proved
  or sourced implication supports a mathematical transfer.
- A finite-counterexample handle is not a promise of a reachable search or a
  claimable prize. Walls apply to stated branches, not automatically every
  mathematical approach to a problem.
- Corrections remain visible. New work does not silently upgrade historical
  record, priority, publication, or solution claims.

## CHRONOS Frontier Board

**Historical July 2026 record.** The table below preserves the recorded claims,
qualifications and retractions. It is not a fresh literature or priority audit.
Its rows also feed the generated book and State of the Frontier, so this README
refresh preserves their contents rather than silently changing published data.
For current research direction, use the [method index](#current-research).

Tier: 🟢 recorded as proven/certified · 🟡 grounded or partial · ⚪ open/in progress
· 🔴 corrected or retracted. Read the linked claim contract and artifact scope.

<details>
<summary>Recorded certificate movements and corrections</summary>

| tier | problem | what CHRONOS contributed | certificate | when |
|---|---|---|---|---|
| 🟢 | **#699** binomial-gcd rows | **property holds for every `n` in `[10⁷, 10⁸)`** — all 90,000,000 rows, every `(i,j)` pair decided exactly, zero counterexamples, 119.53 core-hours. First exhaustive **general-row** sweep past `10⁷` (structured families were already covered to ≈`1.34×10⁸`). Rests on a theorem that large primes never suffice on a pruned row — `p=2` can be the only usable one | [`certificates/erdos-699`](certificates/erdos-699) · PR #129 | 2026-07-27 |
| 🟢 | **#366** 2-full/3-full neighbours | **no 2-full `n` with `n+1` 3-full for `n ≤ 10²⁵`** — 1,620,172,043 cubefull candidates, both orientations, 6.27 core-hours. A 1000× extension of `10²²`, which was a **single unreplayed 2011 OEIS b-file**; this re-derives that region independently. The lever: enumerate the **cubefull** side (`~X^(1/3)`), not the powerful-**pair** side (`~X^(1/2)`) that set the old bound | [`certificates/erdos-366`](certificates/erdos-366) · PR #125 | 2026-07-26 |
| 🟢 | **#743** Gyárfás tree packing | **every one of the 45,376,056 tuples `(T₂,…,T₁₀)` decomposes `K₁₀`** — exhaustive, uncapped, 44 core-seconds. Frontier had stood at `n ≤ 9` since **Fishburn 1983** (43 years); `n=9` reproduced as positive control. Hardest tuples are exactly those with `T₄..T₇` all stars — where Gyárfás–Lehel's coverage stops | [`certificates/erdos-743`](certificates/erdos-743) · PR #126 | 2026-07-27 |
| 🟢 | **#993** tree independence unimodality | **all 23,522,619,475 trees on `n ≤ 30` unimodal**, zero violations, 10.33 core-hours. Includes the **first independent replication** of the `n ≤ 29` frontier (Reynolds, Zenodo v3, 8,691,747,673 trees — single-author, unreplayed until now), reaching his exact total. `n=30` alone is 1.71× that entire prior workload | [`certificates/erdos-993`](certificates/erdos-993) · PR #126 | 2026-07-27 |
| 🟢 | **#552** `R(C4,K1,n)` | certified C₄-free witnesses ⇒ `R(C4,K1,n) = n + ⌈√n⌉ + 1` for `12 ≤ n ≤ 16`; `n=17` closed at `22` (Parsons 1975) | [`certificates/erdos-552`](certificates/erdos-552) · PR #78 | 2026-07-16 |
| 🟢 | **#241** B₃-subset table (A387704) | proved `A387704(n) = max{k : A227358(k) ≤ n−1}` (translation invariance; 0/151 mismatches) ⇒ first jump to 9 at `n=209`; atlas cell **closed by cross-reference** | PR #80 | 2026-07-16 |
| 🟢 | **#13** Erdős–Sárközy | certified exact table `f(1..45)`; `N=17` is the **last** exception to `⌊N/3⌋+1` — an empirical location for Bedert's ineffective threshold | [`certificates/erdos-13`](certificates/erdos-13) · PR #81 | 2026-07-17 |
| 🟢 | **#979** `f₃` / A385316 | **`a(6) > 10¹²` at C2** — exhaustively verified and replayable from this repo (`verify.py --cutoff 1e12`, ~80 s, ~11 GB; reproduces `a(1..5)` as a fail-closed self-check) — past the published `4.99·10¹¹`. A stronger `> 10¹³` sweep exists but its code and ledgers are **not tracked here**, so it is **quarantined from public promotion** pending a self-contained replay packet — see the entry note in the gap map. *(Corrected 2026-07-25: this row previously claimed `> 10¹³` at C1; the second "independent implementation" backing that class lives outside this repository, so a reader could not replay it.)* | [`certificates/erdos-979`](certificates/erdos-979) | 2026-07-19 |
| 🟡 | **#1107** Mollin–Walsh / A056828 | verified **no seventh exception below `10⁶`** to being a sum of ≤3 powerful numbers (`verify.py`, default `N = 10⁶`, ~10 s, dependency-free); the six known exceptions `{7,15,23,87,111,119}` are all `< 120` and are reproduced, powerful-counts cross-checked vs A118896. A wider `10¹⁰` run exists but is **not replayable from this repository**, so it is not the public claim. *(Corrected 2026-07-25: this row previously claimed `10¹⁰`.)* | [`certificates/erdos-1107`](certificates/erdos-1107) | 2026-07-18 |
| 🟡 | **#142** `r₃(N)` | complete 12,349-cell geometric enumeration superseding a flawed 976-cell subset, now certified in-repo as a **construction no-go** — a **foundation only**; self-declared no-bridge, **not** an `r₃(N)` bound | [`certificates/erdos-142`](certificates/erdos-142) · PR #84 | 2026-07-13 |
| 🔴 | **#142** / D15 lemmas | **refuted** `ker π ∩ D = 0` and `q ≥ dim ker π` (two lemmas a bridge attempt rested on) and proved Theorem A in their place — a dead path closed so the next agent does not re-walk it; explicitly **not** an `r₃(N)` bound | [`certificates/erdos-142-kerpi-refutation`](certificates/erdos-142-kerpi-refutation) · PR #101, #102 | 2026-07-24 |
| 🟢 | **#1029 / #77** `R(5,5)` | 42/42 DRAT-certified structural negatives (no witness; rigidity + prime-order orbit collapse), all consistent with `R(5,5) = 43` | [r55-rigidity-certificates](https://github.com/techno-optimist/r55-rigidity-certificates) · DOI [10.5281/zenodo.21305022](https://doi.org/10.5281/zenodo.21305022) | 2026-07-10 |
| 🔴 | **#552** `R(C4,K1,39)` | the `=46` **new-value** claim was **retracted** — DS1 rev.18 lists `46 ≤ f(39) ≤ 47`, OPEN; the 45-vertex witness stands as a re-derivation of Wu–Sun–Radziszowski 2015 | [`certificates/erdos-552-f39`](certificates/erdos-552-f39) | 2026-07-17 |

</details>

The historical board records Erdős cells; it is not the inventory of current
research methods. The full certificate catalogue and caveats are in
[`certificates/README.md`](certificates/README.md). Changes to a recorded claim
need the corresponding evidence and publication-contract update, not just a
README edit.

## The 2026 Jacobian Conjecture crater

The repository preserves its independent verification of Alpöge's 2026 counterexample
in [`certificates/jacobian-conjecture/`](certificates/jacobian-conjecture), with
credit to the external construction. The associated
[crater model](atlas/jc-crater/README.md) separates the exact object check from
propagated mathematical consequences. Its
[root-claim record](atlas/jc-crater/root_claim.json) retains the announcement's
conditional status and source history.

This README refresh does not establish a new peer-review, acceptance or
retraction status for that announcement. Read the dated root record and its
sources before citing the propagation. The reusable
[`crater` machinery](tools/crater.py) and quarantined claims remain available.

## Independent verifications of other people's results

The [Graffiti 284](certificates/graffiti-284-refutation),
[Graffiti 290](certificates/graffiti-290), and
[Keller-map family](certificates/keller-power-weighted-lifts) lanes credit their
external authors and state what the local replay checks. The constructions and
original results are not ours. In particular, the Graffiti 290 claim depends on
the stated gravity convention; its README retains that distinction.

A checksum identifies code bytes; it does not prove that the checker is correct.
Claim contracts, independent semantic replays and negative controls address
separate parts of that trust boundary. Consult each lane's documented coverage.

## Machine-checked formal proofs

Formal artifacts include the [Jacobian](certificates/jacobian-conjecture/lean)
and [Ringel nonstretchability](certificates/ringel-nonstretchability/lean)
projects, plus the newer [binomial-gcd seeds](experiments/astra-lean-seed-20260904/README.md)
and [P699 i=2 work](experiments/astra-i2-complete-20260911/README.md).
Their exact statements, toolchains, dependency pins and axiom checks belong to
the individual bundles. This README update does not claim a fresh build of all
of them or extend a helper theorem to its parent conjecture.

### Formal spine pins (external)

[`atlas/lean_lane.json`](atlas/lean_lane.json) preserves external formalization
checkpoints, including #593 and a deliberately partial #625 checkpoint. A pinned
formalization's scope is distinct from later progress on the underlying problem;
consult the [source update](experiments/astra-freshness-20260911/README.md) rather
than interpreting that older checkpoint as today's full mathematical status.

## Contributing — humans and agents

1. Read [`GRAPH.md`](GRAPH.md), the relevant attack card, and the latest applicable
   source overlay. Read walls before committing compute.
2. Register a bounded lane in [`COORDINATION.md`](COORDINATION.md). Work on a
   separate branch; reach `main` by reviewed PR. Do not force-push another lane.
3. State the exact problem/surface, hypotheses, claim and remaining obligation.
   Prefer an operator another problem can reuse over an unexplained larger run.
4. Preserve proof objects and evidence in git. Supply a replay command, an
   independent oracle where appropriate, and poisoned inputs that fail the same
   acceptance gate. Keep third-party manuscripts outside the patch; cite their
   versions and hashes instead.
5. Add methods to the substrate with honest evidence labels and selector scope.
   Never promote a candidate match to an implication or silently set a status.
6. Keep merged certificates and the production graph frozen unless an explicit
   versioned change is authorized. Do not regenerate evidence in place.
7. Update this README's current-research links and inventory when relevant;
   `tests/test_readme.py` checks counts and entry points. Run the pinned gate,
   reconcile independent review, and verify the pushed branch and CI.

Human corrections, counterexamples and narrower statements are welcome. Open an
issue with the exact claim, source or failing replay; preserve the correction
where the next researcher will find it.

## Provenance and the certificate template

The dataset release **EFA-DR1** is citable at
[10.5281/zenodo.21443635](https://doi.org/10.5281/zenodo.21443635).
See [`CITATION.cff`](CITATION.cff), [`RELEASING.md`](RELEASING.md),
[`LICENSE`](LICENSE) and [`NOTICE`](NOTICE). Cite the exact commit as well for
research added after that release; a later branch is not silently a new DOI
snapshot.

The original deep-audit source and dates remain in
[`atlas/problems.json`](atlas/problems.json). Related verifier-first work includes
[r55-rigidity-certificates](https://github.com/techno-optimist/r55-rigidity-certificates)
and [antipodal-kissing-bounds](https://github.com/techno-optimist/antipodal-kissing-bounds).
Problem history and official status belong to
[erdosproblems.com](https://www.erdosproblems.com), not to this repository's
research labels.

erdos-frontier-atlas

File Explorer

# Use via CDN

# Project Badges

Was this content helpful?

Recent Feedback

Download README