Projects

Research, open-source software, and teaching projects in gravitational waves, machine learning, and mathematical physics. Each project brings together its resources and related writing.

Classical Gravity in Lean

Machine-checked classical gravity with Lean 4 and Mathlib: exact spacetimes, coordinate transformations, and black-hole perturbation systems. Explore the formalization missions and progress on Prove2Me.

Formal Verification Lean General Relativity

Missions on Prove2Me

Hintz2026: Local Equivalence of Kerr–Newman Perturbation Systems

A standalone Lean 4 proof of the local equivalence between Kerr–Newman perturbation systems (1) and (7), for both spin signs, with reproducible source and an axiom audit.

Formal Verification Lean General Relativity

Source on GitHub Prove2Me Mission

Gravitational Waves & AI

系统梳理人工智能方法在引力波数据分析中的应用，从信号识别、参数估计到模拟推断，构建物理驱动与数据驱动相融合的方法论体系。全书五部十二章；提供 HTML 在线阅读、PDF 下载与 LaTeX 源码。

Gravitational Waves Machine Learning Deep Learning

GitHub Repository Download PDF

G-LNS: Generative Large Neighborhood Search for LLM-Based Automatic Heuristic Design

🧬 Revolutionary framework that uses Large Language Models to automatically design Large Neighborhood Search operators for combinatorial optimization. Through synergy-aware co-evolution of destroy and repair operators, achieves near-optimal solutions with reduced computational budgets on TSP and CVRP benchmarks.

Machine Learning Large Language Models Combinatorial Optimization

Go to GitHub Repository arXiv Paper

Evo-MCTS

🧬 Revolutionary LLM-guided framework for automated algorithmic discovery in gravitational wave detection. Combines evolutionary optimization with Monte Carlo Tree Search to achieve 20.2% improvement over domain-specific methods and 59.1% over LLM-based optimization frameworks on MLGWSC-1 benchmark.

Gravitational Waves Machine Learning Algorithm Discovery

Go to GitHub Repository arXiv Paper

GW150914 MCP Signal Search: AI-Powered Gravitational Wave Detection

🌊 AI-powered gravitational wave detection system using Model Context Protocol (MCP) for efficient parameter space exploration. Features optimization client, analysis server, and automated parameter exploration for LIGO GW150914 data with LLM-agent validation.

Gravitational Waves Data Analysis Signal Processing

Go to GitHub Repository Technical Report