Skip to content

audit(erdos-166): mark clean (cycle 5) — R(4,k) Ramsey lower bound integrity verified#21483

Closed
rjwalters wants to merge 0 commit into
mainfrom
audit/erdos-166-2026-05-31-c5
Closed

audit(erdos-166): mark clean (cycle 5) — R(4,k) Ramsey lower bound integrity verified#21483
rjwalters wants to merge 0 commit into
mainfrom
audit/erdos-166-2026-05-31-c5

Conversation

@rjwalters
Copy link
Copy Markdown
Owner

Summary

Re-audit of erdos-166 confirms the axiomatized formalization remains accurate.

  • 269 lines matches lineCount: 269
  • 2 axioms (aks_upper_bound, mattheus_verstraete) matches axiomCount: 2
  • 0 sorries, 0 True stubs
  • status "axiomatized" / badge "axiom" properly flags the two cited bounds without overclaiming

Test plan

  • meta.json sorries field matches actual Lean source count
  • meta.json axiomCount matches actual ^axiom declarations
  • Title and badge accurately reflect axiomatized status

🤖 Generated with Claude Code

@rjwalters rjwalters closed this May 31, 2026
@rjwalters rjwalters force-pushed the audit/erdos-166-2026-05-31-c5 branch from 8c1bac3 to 7513dbf Compare May 31, 2026 18:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant