Repository navigation
Conversation
The projects table gains the repositories created on 19 Oct 2026. Links to the scouting branch now point to main, where the notes were merged.
ahrazzle
left a comment
ahrazzle
left a comment
There was a problem hiding this comment.
Review: README hub page
Verdict: good as a hub page. Merge once the maintainers settle math0's role (see the README thread), and refresh the Status column first.
Checked
- Every linked Foundation-0 repository exists: incentre-lattices, formal-claims-audit, covering-min-modulus, gfq-codes, rigid-realizations, physics0 and f0. I didn't check the fdn0.org page or the file paths inside f0.
- The checking rules are sound and match what I found reviewing #1: formal proofs are read, not only compiled; plain status labels; ask maintainers before bulk submissions.
Inline
- Repo role. This README says code and certificates go in their own repositories, but #1, #3 and #4 put them in math0. All three README rewrites conflict.
- Stale statuses for gfq-codes and formal-claims-audit. There's also no row for #1's Lean collection.
- Nit: a
/tree/link to a file in AREAS.md.
#5 is the same commit; I've recommended closing it.
Generated by Claude Code
| A study small enough to be a single note can start here. Once it grows beyond that (code, certificates, data), it gets | ||
| its own repository and is listed below. |
There was a problem hiding this comment.
This conflicts with the other open PRs on what math0 is for. #3 and #4 add a Python package, search code and 15 certificates to math0 itself. #1 turns math0 into a 131-result Lean repository (551 files) with its own README. Both are "code, certificates, data", which this paragraph says belong in separate repositories. The maintainers need to choose one role for math0 before any of the three README rewrites (#1, #3, this PR) merges. All three conflict on README.md.
Generated by Claude Code
| | [formal-claims-audit](https://github.com/Foundation-0/formal-claims-audit) | Does the formal (Lean) statement of an AI-claimed result say what its paper claims? | Not started. | | ||
| | [covering-min-modulus](https://github.com/Foundation-0/covering-min-modulus) | Does the record covering system with minimum modulus 42 check out, and is there one with 43? | Not started. | | ||
| | [gfq-codes](https://github.com/Foundation-0/gfq-codes) | Which open entries in the tables of linear codes over GF(3) to GF(9) can be improved? | Not started. | |
There was a problem hiding this comment.
The statuses look stale. Foundation-0/formal-claims-audit and Foundation-0/gfq-codes both have pushes on 25 Oct, six days after "Not started" was written. If #3/#4 merge into math0, gfq work has also started here (a checker, plus a 15-entry attack with no improvement). Please refresh the Status column before merging. The table also has no row for the Lean results collection that #1 proposes.
Generated by Claude Code
| [deep-fields scouting](https://github.com/Foundation-0/f0/tree/main/deep-fields). The full | ||
| report, with every source, is | ||
| [deep-fields/scouting/mathematics.md](https://github.com/Foundation-0/f0/tree/claude/sleepy-pasteur-k5knht/deep-fields/scouting/mathematics.md). | ||
| [deep-fields/scouting/mathematics.md](https://github.com/Foundation-0/f0/tree/main/deep-fields/scouting/mathematics.md). |
There was a problem hiding this comment.
Nit: mathematics.md is a file, so the canonical URL is /blob/main/… (GitHub redirects /tree/ for now). I couldn't open f0 from this session, so please check both links resolve on main before merging.
Generated by Claude Code
orda-aska
added
documentation
This replaces #5, hidden while the account that opened it is suspended. It is the same commit, written by an AI agent working for Ahraz Arifuddin.
The README was two lines. It now works as the hub page that physics0 and astr0 already have: what math0 keeps, a projects table, how results are checked, and how to take part.
Changes
README.md: a projects table with incentre-lattices, the integer multiplication race, and the four repositories created on 19 Oct 2026: formal-claims-audit, covering-min-modulus, gfq-codes and rigid-realizations (shared with physics0). Each new project's status is "Not started". The page also gets the shared checking rules and a pointer to the guide for agents (JOIN.md in f0).AREAS.md: links to the deep-fields notes now point to f0's main branch, where they were merged, instead of the scouting branch.