zeta23: consistent formalization-authorship account; de-duplicate CI - #24
Merged
Conversation
The Zeta23/LinAlg headers and the README said those files were written by the paper's authors, while the README and formalization.yaml also said Claude wrote all Lean code. State the actual account everywhere: all Lean code, LinAlg included, was written by Claude; the paper's authors wrote the mathematics, directed the formalization and reviewed it, and wrote no Lean by hand. Comment-only change to the Lean files.
…ator to lean-projects.yml lean-projects.yml now builds every changed project and runs the Comparator bar through .github/scripts/comparator-check.sh, so the dispatch-only build and comparator jobs of zeta23-ci.yml duplicated it. Keep the metadata, licence, README-link, Landrun-wrapper and comparator.json shape checks and the manual doc-gen4 build; point the zeta23 README at comparator-check.sh as well.
Use the paper's wording (orchestrated the Lean work) in all three prose accounts of who did what, instead of 'directed' in one and nothing in the others.
jleder3
approved these changes
Aug 28, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Follow-up to #20 (merged), which laid
zeta23/out as a Palomar template project. Two things:Make the formalization-authorship account consistent — requested by Palomar's automated review of the submitted commit ("The README says Zeta23/LinAlg was written by the paper's authors and incorporated unchanged, while both the README and metadata say Claude wrote all Lean code"). The actual account, now stated everywhere: all Lean code in the repository,
Zeta23/LinAlg/included, was written by Claude; the paper's authors wrote the mathematics, directed the formalization (LinAlg was produced first as a standalone development accompanying §3 of the paper) and reviewed it, and wrote no Lean by hand. Changed: the sevenZeta23/LinAlg/*.leanheaders (comment-only — the comment-stripped sources are byte-identical tomain), the README's "Provenance and attribution",formalization.yaml(automation.notes,acknowledgements;project.authorsstays[Claude]), and theAUDIT.mdrevision note. This commit was pushed to the Lay out zeta23 as a Palomar template project #20 branch after Lay out zeta23 as a Palomar template project #20 had merged, so it never landed.De-duplicate CI — Add per-project CI: build + Palomar comparator check (changed projects only) #19 added
lean-projects.yml, which builds every changed project and runs the Comparator bar through.github/scripts/comparator-check.sh.zeta23-ci.ymlkeeps the template's cheap Palomar checks (formalization.yaml validator, licence detection on both LICENSE files, README submission link, Landrun-wrapper policy, comparator.json shape) and the manual doc-gen4 build, and drops its dispatch-only build and comparator jobs. The zeta23 README points atcomparator-check.shas well.Checks
zeta23-ci.ymlon the previous head passed all three checks (metadata/licence, wrapper, README link); the Lean edits here are comment-only, verified by comment-stripped comparison againstmain.lean-projects.ymlwill selectzeta23for this change (LinAlg headers changed) and run the full build + Comparator bar.After this lands, the merge commit's SHA is the one to resubmit to Palomar (selected project
zeta23, configzeta23/comparator.json).