Skip to content
View f0909172434's full-sized avatar

Highlights

  • Pro

Block or report f0909172434

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
f0909172434/README.md

Chih-Kai Wang | 王治凱

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.

Portfolio · CV · Email

Selected work

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.

Learning and experiments

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.

Open-source contribution

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.

Pinned Loading

  1. honest-ci honest-ci Public

    Make green CI mean the tests you expected actually ran.

    TypeScript 3

  2. finite-witness-webmcp finite-witness-webmcp Public

    Finite-graph counterexample search with inspectable certificates, independent Python replay, and eight shared WebMCP tools.

    JavaScript

  3. rigorgraph rigorgraph Public

    Local-first claim-evidence graphs and deterministic audit reports for AI-assisted research.

    Python 1

  4. proofweave-math-lab proofweave-math-lab Public

    Experimental Python and Lean checker for structured mathematical claims, with inspectable certificates and explicit semantic-alignment limits.

    Python 2

  5. sair-stage2-proof-press sair-stage2-proof-press Public

    Public companion to Lean-checked equational implication solvers: frozen artifacts, released-input evaluations, and an English research paper.

    TypeScript 1

  6. tokenscope tokenscope Public

    An interactive bilingual lab for causal attention, token sampling, and BPE. Inspect the numbers, change the controls, export the experiment.

    TypeScript