ckw whoami
chih-kai@taipei
Python and TypeScript tools for inspectable AI and mathematical research: claims with evidence attached, negative results kept, boundaries stated.
ls -l
Rendered from one catalog file. Open a record to read its raw entry, follow the line link into the repository, and compare the file's hash with the one printed here.
CLI and GitHub Action that checks JUnit reports are present, fresh, and not below a trusted test-count baseline. It does not judge test quality.
$ sed -n '139,147p' src/data/projects.json#L139–L147 ↗
{
"name": "HonestCI",
"kind": "tool",
"status": "v1.0.4 · npm / GitHub Marketplace",
"descZh": "CLI 與 GitHub Action：檢查 JUnit 報告存在、新鮮，且測試數不低於可信基線。不判斷測試品質。",
"descEn": "CLI and GitHub Action that checks JUnit reports are present, fresh, and not below a trusted test-count baseline. It does not judge test quality.",
"repo": "https://github.com/f0909172434/honest-ci",
"links": []
}
record 1 of 19 · sha256 50ccf3b8054d946e…
Local-first Python CLI that links research claims to evidence files and independent review records, checks SHA-256 hashes, and writes offline audit reports. VERIFIED means accepted by the recorded workflow, not true.
$ sed -n '148,157p' src/data/projects.json#L148–L157 ↗
{
"name": "RigorGraph",
"kind": "tool",
"status": "PyPI 1.0.1 · public beta",
"descZh": "本機優先的 Python CLI：把研究主張連到證據檔案與獨立審查記錄，檢查 SHA-256 雜湊，輸出離線稽核報告。VERIFIED 表示通過記錄的流程，不表示結論為真。",
"descEn": "Local-first Python CLI that links research claims to evidence files and independent review records, checks SHA-256 hashes, and writes offline audit reports. VERIFIED means accepted by the recorded workflow, not true.",
"repo": "https://github.com/f0909172434/rigorgraph",
"live": "https://f0909172434.github.io/examples/rigorgraph/math.html",
"links": []
}
record 2 of 19 · sha256 50ccf3b8054d946e…
DeepSeek Harness search plugin that retains citation excerpts and keeps evidence gaps visible. Only verified_search is stable; four extensions are experimental. 250 tests; no independent validation.
$ sed -n '158,166p' src/data/projects.json#L158–L166 ↗
{
"name": "Verified Search",
"kind": "tool",
"status": "v0.1.1 · stable search / experimental extensions",
"descZh": "DeepSeek Harness 檢索外掛：保留引用片段，讓證據缺口可見。只有 verified_search 是穩定版，四個擴充工具仍屬實驗。250 個測試；尚無獨立驗證。",
"descEn": "DeepSeek Harness search plugin that retains citation excerpts and keeps evidence gaps visible. Only verified_search is stable; four extensions are experimental. 250 tests; no independent validation.",
"repo": "https://github.com/f0909172434/dsh-plugin-verified-search",
"links": []
}
record 3 of 19 · sha256 50ccf3b8054d946e…
Patches for DeepSeek Harness on macOS: Seatbelt confinement for shell processes, input-call limits, and per-project memory isolation. Gaps are documented; it is not a universal firewall.
$ sed -n '167,175p' src/data/projects.json#L167–L175 ↗
{
"name": "Second Agent Kit",
"kind": "tool",
"status": "v0.1.4 · macOS only · experimental parts",
"descZh": "DeepSeek Harness 的 macOS 修補：shell 程序的 Seatbelt 限制、輸入呼叫上限、以專案為單位的記憶隔離。缺口都有記錄；它不是萬用防火牆。",
"descEn": "Patches for DeepSeek Harness on macOS: Seatbelt confinement for shell processes, input-call limits, and per-project memory isolation. Gaps are documented; it is not a universal firewall.",
"repo": "https://github.com/f0909172434/dsh-second-agent-kit",
"links": []
}
record 4 of 19 · sha256 50ccf3b8054d946e…
Development-preview toolkit for isolated memory/planning experiments on DeepSeek Harness (Lima VM or Seatbelt), with external judging and cost metering. Results so far come from one small repair task. 85 tests.
$ sed -n '176,184p' src/data/projects.json#L176–L184 ↗
{
"name": "DSH Architecture Lab",
"kind": "tool",
"status": "v0.1.0-dev.9 · development preview",
"descZh": "開發預覽：在 DeepSeek Harness 上跑隔離的記憶／規劃實驗（Lima VM 或 Seatbelt），附外部評判與費用計量。目前的結果只來自一個小型修復任務。85 個測試。",
"descEn": "Development-preview toolkit for isolated memory/planning experiments on DeepSeek Harness (Lima VM or Seatbelt), with external judging and cost metering. Results so far come from one small repair task. 85 tests.",
"repo": "https://github.com/f0909172434/dsh-architecture-lab",
"links": []
}
record 5 of 19 · sha256 50ccf3b8054d946e…
Browser tool that exhaustively searches small graphs (up to 6 vertices) for counterexamples and writes certificates an independent Python script replays. Surviving a bounded search is evidence, not proof.
$ sed -n '185,194p' src/data/projects.json#L185–L194 ↗
{
"name": "Finite Witness",
"kind": "research",
"status": "educational tool · 8 WebMCP tools",
"descZh": "在瀏覽器裡窮舉 6 個頂點以內的小圖找反例，輸出可由獨立 Python 腳本重播的憑證。通過有限搜尋是證據，不是證明。",
"descEn": "Browser tool that exhaustively searches small graphs (up to 6 vertices) for counterexamples and writes certificates an independent Python script replays. Surviving a bounded search is evidence, not proof.",
"repo": "https://github.com/f0909172434/finite-witness-webmcp",
"live": "https://f0909172434.github.io/finite-witness-webmcp/",
"links": []
}
record 6 of 19 · sha256 50ccf3b8054d946e…
Public companion to an equational-implication solver that outputs Lean-checked proofs or finite countermodels. Frozen artifacts accepted 1,669 / 1,669 released inputs with zero model calls.
$ sed -n '195,204p' src/data/projects.json#L195–L204 ↗
{
"name": "SAIR Proof Press",
"kind": "research",
"status": "released-input evaluation · frozen artifacts",
"descZh": "等式蘊涵求解器的公開伴隨站：輸出 Lean 檢查的證明或有限反模型。凍結產物在 1,669 / 1,669 個公開輸入上通過，最終執行沒有呼叫模型。",
"descEn": "Public companion to an equational-implication solver that outputs Lean-checked proofs or finite countermodels. Frozen artifacts accepted 1,669 / 1,669 released inputs with zero model calls.",
"repo": "https://github.com/f0909172434/sair-stage2-proof-press",
"live": "https://f0909172434.github.io/sair-stage2-proof-press/",
"links": []
}
record 7 of 19 · sha256 50ccf3b8054d946e…
Checks author-written structured Markdown proofs against pinned Lean 4 / Mathlib, and reports certification separately from human-confirmed statement alignment. No natural-language translation.
$ sed -n '205,213p' src/data/projects.json#L205–L213 ↗
{
"name": "ProofWeave Core",
"kind": "research",
"status": "experimental · Core 2",
"descZh": "把作者手寫的結構化 Markdown 證明交給固定版本的 Lean 4 / Mathlib 檢查，並把「已認證」與「人工確認語意對齊」分開回報。不做自然語言翻譯。",
"descEn": "Checks author-written structured Markdown proofs against pinned Lean 4 / Mathlib, and reports certification separately from human-confirmed statement alignment. No natural-language translation.",
"repo": "https://github.com/f0909172434/proofweave-math-lab",
"links": []
}
record 8 of 19 · sha256 50ccf3b8054d946e…
Re-ran Goedel-Prover-V2-8B on miniF2F-test through its own released pipeline: pass@32 is 201/244 (82.38%), against the paper's 84.6%. The repository's dataset differs from the paper's in 4 statements; correcting them adds one problem (202/244). Not peer reviewed.
source Raw outputs Upstream issue #8
$ sed -n '214,231p' src/data/projects.json#L214–L231 ↗
{
"name": "Goedel-Prover-V2 audit",
"kind": "research",
"status": "reproducibility audit · draft report",
"descZh": "用官方釋出的流程重跑 Goedel-Prover-V2-8B 的 miniF2F-test：pass@32 為 201/244（82.38%），論文為 84.6%。repo 資料檔與論文所用版本有 4 題陳述不同；改正後多解出 1 題（202/244）。未經同儕審查。",
"descEn": "Re-ran Goedel-Prover-V2-8B on miniF2F-test through its own released pipeline: pass@32 is 201/244 (82.38%), against the paper's 84.6%. The repository's dataset differs from the paper's in 4 statements; correcting them adds one problem (202/244). Not peer reviewed.",
"repo": "https://github.com/f0909172434/goedel-prover-v2-audit",
"links": [
{
"label": "Raw outputs",
"url": "https://github.com/f0909172434/goedel-prover-v2-audit/releases/tag/audit-2026-10-15"
},
{
"label": "Upstream issue #8",
"url": "https://github.com/Goedel-LM/Goedel-Prover-V2/issues/8#issuecomment-6185449509"
}
]
}
record 9 of 19 · sha256 50ccf3b8054d946e…
Deterministic local testbed for how agent memory strategies cope with changing rules. In this pilot, simple retrieval matched more complex strategies (153 / 160) at lower cost.
−Simple retrieval matched the more complex memory strategies; the complexity did not pay for itself.
$ sed -n '232,244p' src/data/projects.json#L232–L244 ↗
{
"name": "RuleShift",
"kind": "research",
"status": "research pilot · 800 paired tasks",
"descZh": "確定性的本機測試床，看 agent 記憶策略如何面對規則改變。這次先導實驗裡，簡單檢索與較複雜的策略表現相當（153 / 160），成本更低。",
"descEn": "Deterministic local testbed for how agent memory strategies cope with changing rules. In this pilot, simple retrieval matched more complex strategies (153 / 160) at lower cost.",
"repo": "https://github.com/f0909172434/ruleshift",
"negative": {
"en": "Simple retrieval matched the more complex memory strategies; the complexity did not pay for itself.",
"zh": "簡單檢索與較複雜的記憶策略表現相當；複雜度沒有換到成效。"
},
"links": []
}
record 10 of 19 · sha256 50ccf3b8054d946e…
Web-policy memory audit workbench: 3,200 model runs and 1,600 controls. The no-LLM controller was stronger than either model. Draft manuscript, not reviewed.
−The no-LLM controller beat both models on the frozen held-out matrix.
$ sed -n '245,257p' src/data/projects.json#L245–L257 ↗
{
"name": "RuleShift-Web",
"kind": "research",
"status": "pre-submission research snapshot",
"descZh": "Web 政策記憶稽核工作台：3,200 次模型執行與 1,600 次對照。不用 LLM 的控制器比兩個模型都強。草稿論文，未經審查。",
"descEn": "Web-policy memory audit workbench: 3,200 model runs and 1,600 controls. The no-LLM controller was stronger than either model. Draft manuscript, not reviewed.",
"repo": "https://github.com/f0909172434/ruleshift-web",
"negative": {
"en": "The no-LLM controller beat both models on the frozen held-out matrix.",
"zh": "在凍結的保留矩陣上，不用 LLM 的控制器勝過兩個模型。"
},
"links": []
}
record 11 of 19 · sha256 50ccf3b8054d946e…
Four-page technical report: a lexical policy-impact predictor scored 0.99 macro-F1 on development data and 0.67 on one held-out packet. Not peer reviewed.
−0.99 on development, 0.67 held out; the full-paper follow-up was stopped under its preregistered rule and frozen as this report.
$ sed -n '258,270p' src/data/projects.json#L258–L270 ↗
{
"name": "RuleDiff negative result",
"kind": "research",
"status": "negative result · technical report",
"descZh": "四頁技術報告：詞彙式政策影響預測器在開發集的 macro-F1 是 0.99，在一組保留資料上掉到 0.67。未經同儕審查。",
"descEn": "Four-page technical report: a lexical policy-impact predictor scored 0.99 macro-F1 on development data and 0.67 on one held-out packet. Not peer reviewed.",
"repo": "https://github.com/f0909172434/rulediff-negative-result",
"negative": {
"en": "0.99 on development, 0.67 held out; the full-paper follow-up was stopped under its preregistered rule and frozen as this report.",
"zh": "開發集 0.99、保留集 0.67；完整論文的後續依預先登錄的規則停止，凍結成這份報告。"
},
"links": []
}
record 12 of 19 · sha256 50ccf3b8054d946e…
Experimental Qwen3.5-4B MLX fine-tune that picks statistical procedures locally. Improves on a simulator benchmark (DGP-Regret −34%) but not on P-Bench or StatQA.
−No improvement on P-Bench or StatQA; only the simulator benchmark moved.
$ sed -n '271,283p' src/data/projects.json#L271–L283 ↗
{
"name": "Charlie Alpha 4B",
"kind": "research",
"status": "experimental v0.3.0 · mixed results",
"descZh": "實驗性的 Qwen3.5-4B MLX 微調，在本機挑選統計程序。在模擬基準有改善（DGP-Regret −34%），在 P-Bench 與 StatQA 沒有。",
"descEn": "Experimental Qwen3.5-4B MLX fine-tune that picks statistical procedures locally. Improves on a simulator benchmark (DGP-Regret −34%) but not on P-Bench or StatQA.",
"repo": "https://github.com/f0909172434/Charlie-Alpha-4B",
"negative": {
"en": "No improvement on P-Bench or StatQA; only the simulator benchmark moved.",
"zh": "P-Bench 與 StatQA 沒有改善；只有模擬基準有變化。"
},
"links": []
}
record 13 of 19 · sha256 50ccf3b8054d946e…
Bilingual in-browser lab: a hand-set one-head 5×5 attention toy, sampling controls (temperature, top-k, top-p), a step-by-step BPE merge demo, and exportable numbers.
$ sed -n '284,293p' src/data/projects.json#L284–L293 ↗
{
"name": "TokenScope",
"kind": "learning",
"status": "educational browser lab",
"descZh": "雙語瀏覽器實驗室：手動設定的單頭 5×5 注意力玩具、取樣控制（temperature、top-k、top-p）、逐步 BPE 合併示範，數值可匯出。",
"descEn": "Bilingual in-browser lab: a hand-set one-head 5×5 attention toy, sampling controls (temperature, top-k, top-p), a step-by-step BPE merge demo, and exportable numbers.",
"repo": "https://github.com/f0909172434/tokenscope",
"live": "https://f0909172434.github.io/tokenscope/?lang=zh-Hant",
"links": []
}
record 14 of 19 · sha256 50ccf3b8054d946e…
Python workshop where learners build a small agent harness in eight steps, offline with a scripted mock model, backed by a 38-module Traditional Chinese curriculum. Not production.
$ sed -n '294,303p' src/data/projects.json#L294–L303 ↗
{
"name": "MiniHarness",
"kind": "learning",
"status": "8-step workshop · zh-TW curriculum",
"descZh": "Python 工作坊：八步做出一個小型 agent harness，離線使用腳本化的模擬模型，附 38 個模組的繁體中文課程。不是生產環境用的。",
"descEn": "Python workshop where learners build a small agent harness in eight steps, offline with a scripted mock model, backed by a 38-module Traditional Chinese curriculum. Not production.",
"repo": "https://github.com/f0909172434/miniharness",
"live": "https://f0909172434.github.io/miniharness/",
"links": []
}
record 15 of 19 · sha256 50ccf3b8054d946e…
A 4:30 short film: at 3 a.m. someone asks an AI "Will she get better?" Three.js rendered CPU-only in headless Chromium; score and sound design synthesised in Python. The README cites sources for the film's historical details and marks what was reconstructed.
$ sed -n '304,314p' src/data/projects.json#L304–L314 ↗
{
"name": "卜 ORACLE",
"kind": "creative",
"status": "v3.0 release · Oct 2026",
"descZh": "4 分 30 秒短片：凌晨三點，有人問 AI「她會好起來嗎？」Three.js 在無頭 Chromium 裡只用 CPU 渲染，配樂與音效用 Python 合成。README 為片中的史料註明出處，並標示哪些是重建。",
"descEn": "A 4:30 short film: at 3 a.m. someone asks an AI \"Will she get better?\" Three.js rendered CPU-only in headless Chromium; score and sound design synthesised in Python. The README cites sources for the film's historical details and marks what was reconstructed.",
"repo": "https://github.com/f0909172434/ORACLE",
"watch": "https://youtu.be/kQH1PZRkn00",
"made": "Three.js r169 · SwiftShader (CPU) · numpy/scipy score",
"links": []
}
record 16 of 19 · sha256 50ccf3b8054d946e…
An original song and hand-painted watercolour music video, 3:35, 67 shots. The score is a Python program; DiffSinger vocals render bit-exactly from fixed seeds; Whisper transcription is used as a diction check.
$ sed -n '315,325p' src/data/projects.json#L315–L325 ↗
{
"name": "病名為AI · The Disease Called AI",
"kind": "creative",
"status": "released · Oct 2026",
"descZh": "原創歌曲與手繪水彩 MV，3 分 35 秒，67 個鏡頭。樂譜是一支 Python 程式；DiffSinger 歌聲用固定種子逐位元重現；用 Whisper 聽寫檢查咬字。",
"descEn": "An original song and hand-painted watercolour music video, 3:35, 67 shots. The score is a Python program; DiffSinger vocals render bit-exactly from fixed seeds; Whisper transcription is used as a diction check.",
"repo": "https://github.com/f0909172434/The-Disease-Called-AI",
"watch": "https://youtu.be/ha-ANfqri6g",
"made": "p5.js + p5.brush · DiffSinger · Kokoro · Whisper QA",
"links": []
}
record 17 of 19 · sha256 50ccf3b8054d946e…
Mili's world.execute(me); staged as a Claude Code session and played live in the terminal. Pure Node, no dependencies; every frame is a function of song time. Unofficial fan work after MisakaZentai's DeepSeek Harness version; the song is not included.
$ sed -n '326,336p' src/data/projects.json#L326–L336 ↗
{
"name": "world.execute(me); · Claude Code",
"kind": "creative",
"status": "fan PV · Oct 2026",
"descZh": "把 Mili 的 world.execute(me); 演成一場 Claude Code 會話，直接在終端機裡即時播放。純 Node、零依賴；每一格畫面都是歌曲時間的函數。非官方同人作品，承接 MisakaZentai 的 DeepSeek Harness 版；不含歌曲音檔。",
"descEn": "Mili's world.execute(me); staged as a Claude Code session and played live in the terminal. Pure Node, no dependencies; every frame is a function of song time. Unofficial fan work after MisakaZentai's DeepSeek Harness version; the song is not included.",
"repo": "https://github.com/f0909172434/world-execute-me-claude-code",
"watch": "https://youtu.be/iEsGiRECytY",
"made": "Node 20, zero dependencies · 24-bit ANSI · braille/sextant canvases",
"links": []
}
record 18 of 19 · sha256 50ccf3b8054d946e…
One animation atlas, two unofficial host packages: a 16-direction animated pet for Codex Desktop, and a DeepSeek Harness plugin that reacts to session state, offline.
$ sed -n '337,350p' src/data/projects.json#L337–L350 ↗
{
"name": "DeepSeek Girl",
"kind": "other",
"status": "Codex v0.1.0 · Harness v0.2.0 · unofficial",
"descZh": "同一份動畫圖集、兩個非官方宿主套件：Codex Desktop 的 16 方向動畫寵物，以及回應 Session 狀態的 DeepSeek Harness 外掛，離線運作。",
"descEn": "One animation atlas, two unofficial host packages: a 16-direction animated pet for Codex Desktop, and a DeepSeek Harness plugin that reacts to session state, offline.",
"repo": "https://github.com/f0909172434/deepseek-girl-codex-pet",
"links": [
{
"label": "Harness plugin",
"url": "https://github.com/f0909172434/dsh-deepseek-girl-pet"
}
]
}
record 19 of 19 · sha256 50ccf3b8054d946e…
✓ 19 of 19 records · projects.json sha256 50ccf3b8054d
ckw verify --keep-negatives
Results that did not go the way I hoped stay public, with the same frozen artifacts as the ones that did.
4 negative results · 0 hidden · each with its frozen artifacts
ls *.md
Longer write-ups kept as Markdown in the profile repository: the problem, the observable result, the engineering decisions, and what the result does not show.
A runner exits 0 while its JUnit report records zero tests; HCI004_ZERO_TESTS blocks it. Why exit codes and test counts are different signals.
Changed evidence bytes surface as RG_HASH_MISMATCH; a changed claim invalidates its old acceptance. A hash answers identity, not sufficiency.
Candidate 39 is C₄. The certificate records the prefix actually searched, not the range requested; people and WebMCP agents inspect the same engine.
Lean certified one obligation; statement alignment stayed UNCONFIRMED. Formal validity and semantic alignment are separate axes and stay separate.
Search routes propose candidates; Lean decides. Released-input results are bound to an evaluator commit, and the claim boundaries say what they do not show.
38 Traditional Chinese modules, fixed checker contracts, and a kept negative result: adaptation improved a dev score while worsening held-out perplexity.
A merged fix that narrows a native-window fallback so unrelated errors stay failures, and repairs standalone helper loading.
git log --graph --oneline
I write the question, the boundary, and what would count as done: which tests, which replay, which hash.
Claude Code and Codex (including Codex Cloud) write most of the code, tests and docs, in branches I review. Most lines in these repositories were typed by an agent; every claim is mine.
Evidence decides, not confidence: tests, independent replay checkers, content hashes. Negative results stay published with the same care as positive ones.
This site and the GitHub profile README are generated from one catalog file; the build fails if they drift.
Claude Code · Codex · Codex Cloud · GitHub Actions · pytest / vitest · Lean 4
ckw play --loop *
Three works from October 2026 where the film, the music and the cut are all source code. Each repository documents its pipeline and its limits.
A 4:30 short film: at 3 a.m. someone asks an AI "Will she get better?" Three.js rendered CPU-only in headless Chromium; score and sound design synthesised in Python. The README cites sources for the film's historical details and marks what was reconstructed.
made with Three.js r169 · SwiftShader (CPU) · numpy/scipy score
An original song and hand-painted watercolour music video, 3:35, 67 shots. The score is a Python program; DiffSinger vocals render bit-exactly from fixed seeds; Whisper transcription is used as a diction check.
made with p5.js + p5.brush · DiffSinger · Kokoro · Whisper QA
Mili's world.execute(me); staged as a Claude Code session and played live in the terminal. Pure Node, no dependencies; every frame is a function of song time. Unofficial fan work after MisakaZentai's DeepSeek Harness version; the song is not included.
made with Node 20, zero dependencies · 24-bit ANSI · braille/sextant canvases
The loops on this page are drawn live in ASCII from the same idea as each film; the films themselves are on YouTube.
ckw log --now --merged
Shipped three works made entirely as code: ORACLE, The Disease Called AI, and world.execute(me).
Audited Goedel-Prover-V2-8B on miniF2F with its own pipeline: 201/244 against the paper's 84.6%, plus a dataset mismatch found and reported upstream.
Froze the RuleDiff negative result as a technical report; the RuleShift-Web manuscript is pre-submission.
Two upstream fixes merged: DeepSeek Harness Desktop and dsh-engram.
Learning Lean 4 / Mathlib through ProofWeave and SAIR.
dsh-tauri/deepseek-harness-desktop#740 Normalise symlinked worktree paths so re-creating a worktree cannot misjudge and delete uncommitted changes.
kenz1117/dsh-engram#4 Trace legacy database claims and add a conservative migration.
EmiyaKatuz/Codex-Dream-Skin-Needy-Girl-Overdose#10 Keep Windows verification failures distinguishable: narrower native-window fallback, standalone helper loading. case study ↗
Only merged pull requests are listed. Dates come from the catalog, not from this page.
cat about.md
I am a B.S. student in the Mathematics Division of the Department of Mathematics and Information Education at National Taipei University of Education, expected 2028, based in Taipei. I build small tools that make a claim checkable: a CI check that reads the test report instead of the exit code, an audit that ties a research claim to the bytes of its evidence, a search that returns the counterexample and the range it searched.
Currently learning Lean 4 and Mathlib through ProofWeave and the SAIR solver work, and reading about formal methods. I am looking for a software engineering or AI internship where tests and evidence decide what ships.