I am Chih-Kai Wang (王治凱), a B.S. student in the Mathematics Education Division at National Taipei University of Education, expected to graduate in 2028.
I work across AI for Mathematics, verifiable reasoning, and reproducible research engineering. My central question is practical: when a proof, computation, model output, or review is offered as evidence, what does it actually license us to claim—and what must remain unresolved?
| Instrument | What you can inspect | Current state |
|---|---|---|
| Finite Witness | A shared graph-conjecture workbench where people and agents search for the same smallest counterexample and preserve a deterministic certificate | Live WebMCP app |
| RigorGraph | Local claim-evidence graphs, deterministic audit, a self-contained offline report, and a GitHub Action | Public beta · 1.0.1 |
| ProofWeave Core | Structured proof certification with formal validity kept separate from natural-language scope | Core package 2.0.0 |
| HonestCI | Whether the JUnit evidence behind green CI is fresh, non-empty, and consistent with a trusted baseline | npm and GitHub Action · 1.0.4 |
| Charlie Alpha 4B | A trilingual statistical procedure-selection model whose release preserves both its DGP gain and benchmark non-improvements | Experimental v0.3.0; later work remains unreleased |
| Verified Search | Bounded current-source retrieval with retained sources, deterministic post-checks, and visible evidence gaps | Stable v0.1.1 plus an experimental snapshot |
The remaining public repositories cover conservative Scientific WorkPlace automation and state-aware open desktop pets for DeepSeek Harness and Codex. Private research repositories and unreleased evaluation artifacts are intentionally absent from this page.
Mathematical reasoning
Automated theorem proving, autoformalization, finite structures, and counterexample search.
Evidence governance
Claim-promotion conditions, negative results, reproducible evaluation, and auditable research agents.
Research engineering
Local-first tools, deterministic reports, source and artifact binding, and explicit safety boundaries.
freeze the claim → attach replayable evidence → state the boundary
- A bounded search is evidence, not a proof.
- A valid formal certificate does not automatically settle the scope of the surrounding prose.
- A green workflow check verifies its declared contract, not universal truth.
- No upgrade, insufficient evidence, and a negative result are outcomes worth preserving.
Taipei, Taiwan · Python · TypeScript · Lean 4 / Mathlib (developing)
I am open to AI4Math research, internships, and open-source collaboration. Contact me at f0909172434@gmail.com or read the one-page CV.