Austin Shen
B.S. Mathematics & Data Science • University of Michigan • GPA 4.0
Researcher in neuro-symbolic AI & formal theorem proving. Building at the intersection of language models and mathematical reasoning.
Math meets Machine Learning
I'm Austin (Zi Jun) Shen, a junior at the University of Michigan studying Mathematics and Data Science with a perfect 4.0 GPA. I work under Prof. Yunong Shi on LeanQC, a neuro-symbolic framework for automated theorem proving in Lean 4.
My research sits at the intersection of formal methods, large language models, and mathematical reasoning. I believe rigorous proof systems and neural networks can be made to work together — and I'm building that bridge.
Beyond research, I've shipped production software at BotSmart (LLM security evaluation) and Innovation AI (full-stack AI product). I'm always looking for the next hard problem.
Tools & Technologies
Languages
Frontend / Backend
Infra / Cloud
Data / AI
Research Projects
LeanQC — Autoformalization & Formal Theorem Proving
Developing a neuro-symbolic framework to formalize informal mathematical statements into Lean 4 code. The DSP-Plus (Draft, Sketch, Prove) architecture uses LeanTree with structured generation and an iterative compiler-feedback pipeline. Ablation studies conducted on MiniF2F and ProofNet (Pass@k metric).
- DSP-Plus architecture: Draft → Sketch → Prove with LeanTree
- Structured generation + iterative compiler feedback
- Benchmarked on MiniF2F and ProofNet (Pass@k)
Voice-Controlled AR Hand Assistant
Built a multi-modal AR pipeline on Meta Quest 3 using the Meta XR SDK. Integrates YOLOv11 for real-time object detection, GPT-4o for natural language understanding, CLIP for zero-shot classification, and Moondream for visual question answering.
- Meta Quest 3 + Meta XR SDK deployment
- YOLOv11 real-time object detection
- GPT-4o + CLIP + Moondream multi-modal pipeline
Published Work
Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
Austin Shen, Yunong Shi
Identifies that parallel tactic search reconstructs proof states repeatedly, consuming over 99% of per-branch processing time. Introduces proof-state snapshotting — capturing an elaborated proof state once and reusing it across search branches via a Lean 4 language server extension. Achieves 5.6–50× wall-time speedup (avg 14×, median 9.7×) on miniF2F-v2 benchmarks.
Industry Experience
Software Engineer
BotSmart
Built LLMAE — an automated LLM prompt attack evaluation platform. Designed the full backend with Django and containerized the entire stack with Docker for reproducible deployments.
Full Stack Engineer
Innovation AI
Architected and shipped Firebase Cloud Functions, Node.js REST APIs, and integrated a Stripe payment pipeline for a production AI product.
Have a project in mind?
I'm open to research collaborations, internship opportunities, and interesting engineering problems.