polish: highlight TheoremPath site + iOS companion in FormalSLT README#7
polish: highlight TheoremPath site + iOS companion in FormalSLT README#7Robby955 wants to merge 1 commit into
Conversation
Adds an above-the-fold hero (mermaid diagram), a "Part of the TheoremPath family" section describing the live site (theorempath.com) and the native iOS companion (theorem-path-ios), and "For researchers" / "For students" audience callouts. Adds an About footer. Adds three CI-checked badges (theorems / modules / lines) backed by a new scripts/generate_badge_counts.py and three docs/badges/*.json blobs. CI gains a "Check badge counts" step that mirrors the existing generate_proof_frontier_manifest.py --check pattern, so counts cannot silently drift. No changes to the existing v0.1 surface table, scope, install, release-candidate checks, audit commands, module map, roadmap, dependencies, contributing, citation, or license sections. Counts at this snapshot (verified on disk against origin/main 108a139): - 60 FormalSLT/*.lean files - 85 FormalSLT/ + examples/ *.lean files - 33,427 total Lean lines - 673 theorem + lemma declarations - 0 sorry, 0 admit, 0 custom axioms Audit: - 0 banned phrases per AGENTS.md rule #2 - 0 em-dashes per rule #3 (0/3 budget used) - 0 Claude / agent / dispatch mentions per rule #4 - 0 emoji in README body
📝 WalkthroughWalkthroughThe PR adds an automated badge-generation system for the FormalSLT repository. A new Python script scans Lean source files to collect theorem, module, and line-count metrics, produces Shields.io-compatible badge JSON payloads, and integrates metric verification into CI. The README is enriched with dynamic badge endpoints, TheoremPath ecosystem context, and documentation of the badge regeneration process. ChangesBadge Metric Generation and Documentation
Estimated code review effort🎯 2 (Simple) | ⏱️ ~12 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@README.md`:
- Around line 527-534: The About paragraph for "FormalSLT" currently mixes
repository/product description with a workshop acceptance claim; edit the README
About section by splitting that paragraph into two distinct parts: one sentence
or bullet describing the library and its role (e.g., "FormalSLT is authored by
Rob Sneiderman... verification spine for related research..."), and a separate
sentence or bullet that states the workshop acceptance (e.g., "The author has an
accepted ICML 2026 Culture × AI workshop poster and upstream contributions to
mathlib4"), ensuring the product/repo claims and the ICML/workshop claim are
clearly separated.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro Plus
Run ID: 58fb1dd4-9b89-4709-be40-452be279ca2d
📒 Files selected for processing (6)
.github/workflows/ci.ymlREADME.mddocs/badges/lines.jsondocs/badges/modules.jsondocs/badges/theorems.jsonscripts/generate_badge_counts.py
| FormalSLT is authored by **Rob Sneiderman** | ||
| ([Robby955](https://github.com/Robby955) on GitHub, | ||
| [robbysneiderman.com](https://robbysneiderman.com)). The library underwrites | ||
| the public TheoremPath learning surfaces and is the verification spine for | ||
| related research on finite-sample concentration, PAC-Bayes, and statistical | ||
| learning theory. The author is an applied/mathematical statistician with an | ||
| accepted ICML 2026 Culture × AI workshop poster and upstream contributions to | ||
| mathlib4. |
There was a problem hiding this comment.
Separate workshop claim from product/repo claims in About section.
This paragraph mixes public-repo/product description with the workshop acceptance statement; split them into distinct sentences or bullets by claim type.
Suggested rewrite
-FormalSLT is authored by **Rob Sneiderman**
-([Robby955](https://github.com/Robby955) on GitHub,
-[robbysneiderman.com](https://robbysneiderman.com)). The library underwrites
-the public TheoremPath learning surfaces and is the verification spine for
-related research on finite-sample concentration, PAC-Bayes, and statistical
-learning theory. The author is an applied/mathematical statistician with an
-accepted ICML 2026 Culture × AI workshop poster and upstream contributions to
-mathlib4.
+FormalSLT is authored by **Rob Sneiderman**
+([Robby955](https://github.com/Robby955) on GitHub,
+[robbysneiderman.com](https://robbysneiderman.com)).
+
+Public-repo/product claim: this library underwrites the TheoremPath learning
+surfaces as their Lean verification spine.
+
+Workshop-paper claim: the author has an accepted ICML 2026 Culture × AI
+workshop poster.
+
+Other contribution claim: upstream contributions to mathlib4.As per coding guidelines: “Keep workshop-paper claims, public-repo claims, and future-venue claims separate in documentation to avoid blurring what is proved today with what is planned next”.
📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| FormalSLT is authored by **Rob Sneiderman** | |
| ([Robby955](https://github.com/Robby955) on GitHub, | |
| [robbysneiderman.com](https://robbysneiderman.com)). The library underwrites | |
| the public TheoremPath learning surfaces and is the verification spine for | |
| related research on finite-sample concentration, PAC-Bayes, and statistical | |
| learning theory. The author is an applied/mathematical statistician with an | |
| accepted ICML 2026 Culture × AI workshop poster and upstream contributions to | |
| mathlib4. | |
| FormalSLT is authored by **Rob Sneiderman** | |
| ([Robby955](https://github.com/Robby955) on GitHub, | |
| [robbysneiderman.com](https://robbysneiderman.com)). The library underwrites | |
| the public TheoremPath learning surfaces and is the verification spine for | |
| related research on finite-sample concentration, PAC-Bayes, and statistical | |
| learning theory. | |
| The author has an accepted ICML 2026 Culture × AI workshop poster and has | |
| contributed upstream to mathlib4. |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@README.md` around lines 527 - 534, The About paragraph for "FormalSLT"
currently mixes repository/product description with a workshop acceptance claim;
edit the README About section by splitting that paragraph into two distinct
parts: one sentence or bullet describing the library and its role (e.g.,
"FormalSLT is authored by Rob Sneiderman... verification spine for related
research..."), and a separate sentence or bullet that states the workshop
acceptance (e.g., "The author has an accepted ICML 2026 Culture × AI workshop
poster and upstream contributions to mathlib4"), ensuring the product/repo
claims and the ICML/workshop claim are clearly separated.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1f41eecf0d
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| > Every theorem here has a matching learning surface on the live site | ||
| > [theorempath.com](https://theorempath.com), and the same checked | ||
| > statements feed the native iOS companion at | ||
| > [theorem-path-ios](https://github.com/Robby955/theorem-path-ios). |
There was a problem hiding this comment.
The linked TheoremPath verification page at https://theorempath.com/lean currently advertises only 56 verified entries and describes that manifest as a scoped subset, while this repo reports hundreds of Lean theorem/lemma declarations. For users following this integration, the claim that every theorem in the repo has a matching learning surface is false until the site indexes the whole repo, so this should be narrowed to the public-facing theorem subset.
Useful? React with 👍 / 👎.
1 participant
What this changes
research-ops-2026/submissions/SUBMISSIONS_TRACKER.md).scripts/generate_badge_counts.pyanddocs/badges/{theorems,modules,lines}.json. CI gains aCheck badge countsstep that mirrorsgenerate_proof_frontier_manifest.py --check.What this does NOT change
The pre-existing v0.1 surface table, scope, install, release-candidate checks, audit commands, module map, roadmap, dependencies, contributing, citation, and license sections are untouched.
Verified counts at this snapshot (origin/main
108a139)FormalSLT/*.leanfilesfind FormalSLT -name '*.lean' | wc -lFormalSLT/+examples/*.leanfilesfind FormalSLT examples -name '*.lean' | wc -lfind ... -name '*.lean' | xargs wc -ltheorem/lemmadecls.leanfilessorry/admit/ custom axiomsAudit
27 sister sitesclaim dropped for lack of on-disk evidence; ICML claim reduced to the single tracker-confirmed acceptance).Follow-ups (not blocking this PR)
33,427 linestext. The new badge row is the live source of truth; the prose number is a snapshot. Future polish pass can drop or hyperlink.theorem-path-ios.theorem-path.Summary by CodeRabbit
New Features
Documentation