anuna-research/cbcl-rs
1
0
Fork 0
Code Issues 2 Pull requests Projects Packages Wiki Activity Actions

Address proof gaps in Lean 4 formalization #1

Merged
hugooconnor merged 0 commits from refs/pull/1/head into main 2026-03-20 04:00:20 +00:00
Conversation 0 Commits - Files changed -
hugooconnor commented 2026-03-20 03:59:36 +00:00 (Migrated from codeberg.org)
Copy link
  • Parser: prove allSExpr_wellFormed and connect WellFormedSExpr to parse output
  • Serializer: add SafeSymbol predicate, RoundTrippable' characterization, concrete tests
  • R1: add computable DFS-based checkNoCycles cycle detector with soundness proof
  • R2: add boundedEvalFull that recursively processes all list children with depth bound theorem
  • DetParser: golf langDetParser_step_state_lt/ne_zero from 152 to 2 lines each

All files compile with zero errors, zero warnings, zero sorries, no custom axioms.

Co-Authored-By: Claude Opus 4.6 (1M context) noreply@anthropic.com

- Parser: prove allSExpr_wellFormed and connect WellFormedSExpr to parse output - Serializer: add SafeSymbol predicate, RoundTrippable' characterization, concrete tests - R1: add computable DFS-based checkNoCycles cycle detector with soundness proof - R2: add boundedEvalFull that recursively processes all list children with depth bound theorem - DetParser: golf langDetParser_step_state_lt/ne_zero from 152 to 2 lines each All files compile with zero errors, zero warnings, zero sorries, no custom axioms. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Sign in to join this conversation.
Reviewers
No reviewers
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
anuna-research/cbcl-rs!1
No description provided.