OUKC への貢献ガイド
概要 / Description
日: OUKC への貢献方法. issue / PR / discussion / Lean 4 contribution / paper co-authorship / translation の各 channel.
EN: How to contribute to OUKC. Issues, PRs, discussions, Lean 4 contributions, paper co-authorship, translations.
Contributing to Open Universal Knowledge Commons (OUKC) & Rei & Claude
OUKC への貢献ガイド
Welcome! / ようこそ! Below is the practical guide.
🚀 Quick start / 最短手順
1. Lean 4 formal proof contribution
# Clone the repo
git clone https://github.com/fc0web/rei-aios.git
cd rei-aios/data/lean4-mathlib
# Create a new file
mkdir -p CollatzRei/YourField
$EDITOR CollatzRei/YourField/MyTheorem.lean
# Verify it builds
lake env lean CollatzRei/YourField/MyTheorem.lean
# → exit 0 expected for TRUE_PROVED
# Open a PR
git checkout -b feat/your-theorem
git commit -m "Add my theorem (TRUE_PROVED)"
git push origin feat/your-theorem
2. META-DB knowledge entry contribution
# META-DB structure (see docs/metadb-v3-0-spec.md)
cd data/open-problems/
# Pick a tier:
# tier1/ - World-public open problems (Wikipedia/Erdős/etc.)
# tier4/ - Gaps (things Claude/Rei/community feels are missing)
# tier7/ - Latest axioms (14 fields × catalog entries)
# tier8/ - Impossibility map (formalization-resistant)
# Add a JSON entry per the schema
$EDITOR tier7/<field>/your-entry.json
# Validate schema (script TBD)
npx tsx scripts/validate-metadb-entry.ts data/open-problems/tier7/<field>/your-entry.json
3. Paper contribution
# Drafts go in papers/
$EDITOR papers/paper-<N>-your-topic.md
# Follow 4+7 element structure (see feedback_paper_four_element_structure.md)
# Required: A.1 Findings / A.2 Proofs / A.3 Honest positioning / A.4 Required platform links
📋 Required for every contribution
Mandatory checklist
- Mechanical verification (Lean 4 / Coq / equivalent) for proof claims
- D-FUMT₈ outcome tag in commit message / file header
- AI attribution if AI used substantially (
Co-Authored-By:line) - Honest scope — no overclaim, comparison denominators included
- Peace Axiom #196 respected (no military / harm use)
Commit message format
<scope>: <short description>
<body explaining what + why>
D-FUMT₈ outcome: <TRUE_PROVED | PARTIAL | INFINITY | FALSE | NEITHER | NEITHER_SELF>
Verification: <e.g., lake env lean exit 0, sorry=0, axiom=0>
Co-Authored-By: <AI models if used>
Example:
brocard: Extend n=131..150 (TRUE_PROVED)
24 new theorems following STEP 1017 pattern.
All verified via lake env lean exit 0.
D-FUMT₈ outcome: TRUE_PROVED
Verification: lake env lean ./CollatzRei/Step1018BrocardExtended150.lean exit 0, sorry=0, axiom=0
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
🌐 Multilingual contribution / 多言語貢献
Japanese ↔ English / 日英バイリンガル
- Code comments: English standard (international convention) but Japanese OK for domain-specific terms
- Documentation: Bilingual encouraged (this CONTRIBUTING.md is an example)
- Discussion: Japanese OR English on community channels (Discord/Matrix TBD)
- Paper titles: English primary, Japanese subtitle welcome
Other languages / 他言語
- 中文 / 한국어 / Other: Translation contributions welcomed (CC-BY 4.0)
- Open a PR with
lang/zh-CN/CHARTER.mdetc.
🤖 AI-assisted contribution workflow / AI 支援ワークフロー
Recommended pattern
- Human selects the theorem / claim / topic to formalize
- AI generates draft (Lean 4 proof / META-DB JSON / paper section)
- Mechanical verification runs (
lake env lean/ schema validate) - Human reviews + tags D-FUMT₈ outcome
- Human commits with attribution
Anti-pattern (DO NOT DO)
- AI generates 100 PRs in batch and submits all → "AI slop" rejection
- AI claims TRUE_PROVED when build fails → false attribution
- Hide AI involvement → undisclosed chain violation
🔍 Code review / コードレビュー
What reviewers check
- Does it build? (
lake env lean/ equivalent) - Is the D-FUMT₈ tag accurate?
- Is AI attribution present and accurate?
- Is scope honest (no overclaim)?
- Does it respect Peace Axiom #196?
- Is the contribution net-positive for the commons?
Turnaround time
- Trivial commits (TRUE_PROVED + correct tag): Same-day approval (founder review)
- Complex contributions: 1-7 days
- Year 2+ with maintainer team: faster
🆕 First-time contributor / 初回貢献者
Recommended starter contributions:
- Translate part of CHARTER.md or POLICY.md to your native language
- Add a META-DB Tier 7 entry for your field of expertise
- Verify an existing TRUE_PROVED theorem independently and report
- Propose a Tier 4 (gap) — something you feel OUKC should cover but doesn't
These build trust without requiring deep Lean 4 expertise upfront.
💬 Communication / コミュニケーション
Day 1 channels — primary
- GitHub Discussions (primary forum):
github.com/fc0web/rei-aios/discussions★ recommended - GitHub Issues (bug reports + feature requests):
github.com/fc0web/rei-aios/issues - Email: fc2webb@gmail.com (Founder, until governance scales)
- Documentation site:
rei-aios.pages.dev/#/oukc/ - Note (popular):
note.com/nifty_godwit2635
Year 1+ optional additions (on demand)
- Zulip (research chat) — added when real-time research conversations grow
- Discord (casual chat) — added when voice / casual community emerges
We intentionally start with GitHub Discussions only. It's zero-setup, integrated with the codebase, supports Markdown + KaTeX math + Lean 4 syntax, and uses the GitHub account contributors already have. We can add Zulip / Discord later when scale warrants.
📜 License
By contributing, you agree your contribution is licensed under:
- Code: AGPL-3.0 (with commercial dual-license option — contact founder)
- META-DB entries: CC-BY 4.0
- Documentation: CC-BY 4.0
- Lean 4 contributions: Apache 2.0 (Mathlib-compatible if upstream-suitable)
❓ Questions
If your question isn't covered here, open a GitHub Discussion or email the founder. We are early — your question helps us improve this guide.
Co-Authored-By: 藤本伸樹 / Claude Code (Anthropic) / Rei-AIOS
⧯ Open Interactive Rei-AIOS (SPA)