PN-lean
Formal, machine-checked proofs in Lean 4: Sylvester, Schur (complete), prime gaps, Jacobsthal j(2310)=14, and the verified math core of a centriole geometric-aging model (OU, alpha≈0.97)
What XERJ indexed
Snapshot
The whole repository at commit 5554246b21. It is the newest commit on master.
Selected work
Licence
The repository
LICENSE file checked at the pinned commit; the author agreed to inclusion.
The XERJ corpus
The owner added it on hub.xerj.org after signing in with GitHub, on 2026-10-28. Same terms as the repository. Answers name the repo, the commit and the file:line.
selected for the XERJ Corpus Hublicence clearedsuggested use: adapt with attribution
The prompt
Paste it into your AI agent. It clones djabbat/PN-lean at the pinned commit and indexes it on your machine.
Search the GitHub repository djabbat/PN-lean with XERJ (https://hub.xerj.org/corpus/djabbat--pn-lean). Run these in a shell, in order, and check each result before the next: 1. xerj --help (success: it prints usage). If xerj is missing: curl -fsSL https://xerj.org/get | sh 2. git clone https://github.com/djabbat/PN-lean PN-lean && git -C PN-lean checkout 5554246b21c25fe07b83c772aa878ce019539150 3. Start a local node and leave it running: xerj --insecure --data-dir ./xerj-data 4. xerj autoindex ./PN-lean --url http://127.0.0.1:9200 --prefix pn-lean --progress plain 5. xerj autoindex map --url http://127.0.0.1:9200 Then answer my question from the indexed files and cite the ax_path of every hit. Query syntax: https://xerj.org/llms.txt Licence: Apache-2.0. Keep the copyright notice and credit the authors.
Related
Jaba TqemaladzeAPI design and specification corporaATOMSLab/LeanSMILESThe-Last-Math-Competition/The-Last-Math-Competitionformal-applied-math/formal-mathfin
Stats: GitHub API, fetched 2026-10-31. Snapshot: the git tree at the pinned commit. Selected work and consent: the XERJ registry.