I build Python and TypeScript tools that make AI and mathematical research results inspectable and reproducible.
I am a B.S. student in the Mathematics Division, Department of Mathematics and Information Education at National Taipei University of Education, expected 2028. Based in Taipei; open to software engineering and AI application internships.
| Project | What it does | Explore |
|---|---|---|
| HonestCI | Checks that the JUnit evidence behind green CI is fresh, non-empty, and consistent with a trusted baseline. | Source |
| Finite Witness | Search finite graphs for counterexamples, save certificates, and replay the finite search prefix with an independent Python checker. | Try it |
| RigorGraph | Connect research claims to evidence, audit file integrity and review records, and generate an offline report. | Try it |
| ProofWeave Core | Turns author-supplied structured proofs into inspectable certification runs while separating formal validity from semantic scope. | Source |
| SAIR Proof Press | Public companion to Lean-checked equational implication solvers, with frozen artifacts, released-input evaluation and an English paper. | Try it |
| TokenScope | Change attention, sampling, and BPE controls, inspect the arithmetic, and export or replay an experiment. | Try it |
HonestCI checks test-execution evidence. RigorGraph audits evidence and review records. ProofWeave checks an explicit formal target with Lean; semantic alignment remains a separate question.
MiniHarness teaches agent engineering through an eight-step workshop with a Traditional Chinese prerequisite curriculum. Charlie Alpha records statistical procedure-selection experiments, including negative results. Verified Search retains retrieval sources; its extended tools remain experimental.
I contributed a merged Windows verification fix to Codex Dream Skin: unrelated native-window errors remain failures, and standalone verification loads its helpers correctly. I also maintain DeepSeek Girl for Codex and its Harness adapter, built around one animation atlas.
Python · TypeScript · GitHub Actions · JSON Schema · MLX. Developing Lean 4 / Mathlib skills through formal-checking and research projects.


