B.S. student, Mathematics Education Division, Department of Mathematics and Information Education, National Taipei University of Education. Expected 2028.
Taipei, Taiwan | Email | GitHub
I work at the intersection of AI for Mathematics, verifiable reasoning, and reproducible research engineering. I build deterministic tools that keep computational evidence, formal certification, independent review, and mathematical resolution as separate states rather than collapsing them into one confidence score.
Model agreement is not proof. Numerical evidence is not a theorem. Every promoted claim should have traceable dependencies and an independently checkable basis.
| Destination | Entry point | Current status |
|---|---|---|
| Flagship research | ClaimPromoteBench | Public alpha; no model results are reported. |
| Technical report | NOT YET PUBLISHED | A link will be added only after a reproducible pilot and public draft exist. |
| Code and data | ClaimPromoteBench alpha, ProofWeave, RigorGraph, HonestCI | Alpha: 20 controlled pairs / 40 synthetic instances; no model results. |
| CV | One-page CV | Updated August 2026. |
Policy-Governed Evidence-State Transitions for Mathematical Research Agents
Research question: Can a machine-checkable evidence ledger and a versioned deterministic transition gate reduce invalid claim promotion while preserving valid promotion?
The planned benchmark evaluates evidence-state transitions rather than general truth classification or abstention. It is designed to separate an agent's proposed action from the effective action after a deterministic gate, and to use counterfactual pairs to test both invalid and valid promotions.
Current status: public 20-pair / 40-instance alpha for validating the schema, deterministic oracle, controlled-pair design, offline baselines, gate semantics, and evaluation pipeline. No model experiment, completed v1 benchmark, technical report, external review, or independent reproduction is claimed here.
| Project | What can be checked | Public status |
|---|---|---|
| ProofWeave Core v2 | Model-independent parsing of mathematical claims and proofs; deterministic Lean/Mathlib certificate checks; separate certificate, natural-language alignment, and lifecycle states | Repository release v0.1.0; Core package 2.0.0 |
| RigorGraph | Local-first claim-evidence graphs, deterministic audits, provenance and hash checks, and offline reports | Public beta; package 1.0.1 |
| HonestCI | Checks fresh JUnit evidence and detects missing, stale, zero-test, and reduced-count results in CI | Stable package and GitHub Action; 1.0.4 |
These tools check workflow evidence and formal artifacts within their documented boundaries. They do not turn a numerical scan, green CI run, reviewer decision, or model output into mathematical truth.
AI for Mathematics | automated theorem proving | autoformalization | verifier-guided research agents | evaluation and calibration | reproducible scientific computing | nonlinear differential equations | bifurcation theory
Python | TypeScript | SymPy | LaTeX | JSON Schema | GitHub Actions | Lean 4 / Mathlib (developing)
I am preparing for research-based graduate study and seeking opportunities to contribute to AI4Math, theorem-proving, and trustworthy evaluation projects. For research, internship, or open-source collaboration, contact f0909172434@gmail.com.