Projects

Public research software and formalization work.

Projects

Public research software and formalization work

These projects link only to public repositories and documentation. Their descriptions summarize the available materials and do not claim completed research results beyond them.

Current research

Formal representations

Lean 4 · Formal language

LeanArabic

A Lean 4 feasibility project for representing a published fragment of Arabic pregroup grammar and producing machine-checkable grammatical derivations. The public repository documents both its proof-producing reducer baseline and its current scope limits.

  • Lean 4
  • Pregroup grammar
  • Proof-producing reduction

Research software

Verification-oriented tools

Lean 4 · AI reasoning verification

FalconVerifier

A public software project for checking formalized reasoning steps with Lean 4 and recording an assurance trace. Its documentation explicitly distinguishes verified, refuted, unknown, and ill-formed outcomes, and includes a semantic-faithfulness audit for certain LLM translations.

  • Lean 4
  • Assurance traces
  • Semantic-faithfulness audit

Kotlin Multiplatform · Lean 4

ProofLens

A Kotlin Multiplatform application for proposing and checking Lean 4 proofs across Android, desktop, and web targets. The public repository documents a client/server design in which the Lean kernel is the proof-checking authority.

  • Kotlin Multiplatform
  • Lean 4
  • Proof checking

Selected earlier work

Formal-verification experiments

Lean 4 · Algebraic topology

CB-Attractor

A public Lean 4 project for formal-verification experiments on ReLU neural-network decision regions, alongside a formalization component in algebraic topology. The repository identifies Hongwei Wang in its project context; this description does not make claims beyond the repository's public documentation.

  • Lean 4
  • Algebraic topology
  • Neural-network decision regions

Cubical Agda remains part of my current research interests and tools; no standalone public project is listed until its materials have been reviewed and approved.