automath: refresh 3 Q2 focus regions with current operational state#12
Merged
loning merged 2 commits intoMay 18, 2026
Merged
Conversation
Three 2026 Q2 focus regions for Automath: - Automath-Oracle-Pipeline: relabeled '自动化论文流水线 (Oracle)', focus=true - Automath-Open-Problem-Outreach: NEW, seed-tier, attacks external open problems - Automath-Social-Auto-Publish: NEW, public-tier, NotebookLM + SlideSync + Playwright Douyin pipeline (13 videos scheduled)
Update descriptions to reflect operational state on real branches. Three nodes marked Q2 focus (red border): - Automath-Oracle-Pipeline (public, focus): automated paper authoring + review + submission. Active on dev-automation-clean / dev-automation- integration, 11 merged PRs in Q2. - Automath-Open-Problem-Outreach (scoped, focus): derive-loop targets external open problems → Lean proofs + community outreach. 7 PRs merged across automate-outreach / outreach-clean / distill-clean / openproblem-target. - Automath-Social-Auto-Publish (public, focus): ancient-texts social pipeline at ChronoAIProject/omega-ancient-texts-analysis. 13 I-Ching videos scheduled to Douyin (2026-05-09 → 05-22), three-leg verdict JUDGEMENT + COVER_VERIFY + QUEUE_VERIFY. Upstream Lean4-Core / Theorem-Library / AI-Derive-Loop kept as deps, descriptions untouched.
cdb5b4f to
2e0ce9d
Compare
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
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.
按 region-map 单一事实源原则,把 Automath 三大 Q2 focus 节点对齐到代码里的真实自动化状态。三条管线当前都在自动化运行中。
改动
Automath-Oracle-Pipeline自动化论文流水线tools/autoresearch/run_overnight.py自主 Lean 4 formalization 循环;.github/workflows/daily-build.ymlpush 到 dev 自动触发;Live autoresearch YouTube 直播;dev-automation-clean (#45 Oracle Pipeline v2) + dev-automation-integration(Q2 共 10 个合并 PR)Automath-Open-Problem-Outreach公开问题攻坚与社区对接tools/community-outreach/pipeline v23(preflight + impact gate + profile judge);OUTREACH_LOG 显示 8 个已完成对接:teorth/analysis #494、teorth/equational_theories #364 + #418 + PR #1435、mysticflounder #1、automath #38 跟进;进行中目标:Heath Sanchez & Israel Cazares (SAIR)、Terence Tao、google-deepmind/formal-conjectures;8 个 outreach 已反哺到 paper appendixAutomath-Social-Auto-Publish自动化社交媒体宣发Outreach 从
scoped升到bridged—— 因为 8 个 outreach 已经分别完成上游提交(PR/issue/issue comment 等),并且每条都反哺到 paper appendix 形成闭环(典型的 upstream/downstream issues closed + integrated)。不动的部分
Automath-Lean4-Core/Automath-Theorem-Library/Automath-AI-Derive-Loop保留原描述,只作为上游依赖。验证
python3 tools/validate_regions.py→OK: regions.json valid (70 regions)gh_query指向真实分支或 repo,可被 weekly audit 对账