I build Python and TypeScript tools for reliable testing, interactive applications, and AI-assisted research.
I am a B.S. student in the Mathematics Education Division at National Taipei University of Education, expected to graduate in 2028. I am based in Taipei and looking for software engineering and AI application internships.
| Project | What I built | Explore |
|---|---|---|
| Finite Witness | A browser workbench that searches finite graphs for counterexamples. People and agents use the same search engine through the UI and eight WebMCP tools. | Try it · Source |
| HonestCI | A TypeScript CLI and GitHub Action that checks whether JUnit test reports are present, fresh, non-empty, and consistent with a trusted baseline. | Demo · Source |
| RigorGraph | A Python CLI that connects research claims to evidence, checks record integrity, and generates a self-contained offline report. | Open report · Source |
| ProofWeave Core | Experimental Python tools for checking structured mathematical claims with Lean and retaining inspectable certification artifacts. | Actual run · Source |
| SAIR Proof Press | A public companion to Lean-checked solvers for equational implication, with frozen artifacts, evaluation summaries, and an English research paper. | Project site · Source |
| MiniHarness | 38 Traditional Chinese lessons, an eight-step harness workshop, quizzes, assignment checks, and a trainable tiny Transformer. | Interactive demo · Workshop |
Finite Witness · HonestCI · RigorGraph · ProofWeave · SAIR Proof Press · MiniHarness · External Windows contribution
I contributed a merged Windows verification fix to Codex Dream Skin. The change narrowed native-window fallback handling so unrelated errors remained failures, and repaired helper loading in standalone verification.
- Python, TypeScript, JavaScript, GitHub Actions, JSON Schema, and MLX.
- Lean 4 / Mathlib: developing through proof-checking and research projects.
- AI for mathematics, finite counterexample search, developer tools, and reproducible evaluation.
I also work on statistical procedure-selection experiments and source-retaining search tools.
My project reports keep measured results and limitations together. A finite graph search has a declared bound, a Lean certificate applies to its exact formal target, and experimental model results retain their negative findings.
For internships or collaboration, contact f0909172434@gmail.com.