AI Researcher | Scientific Machine Learning (SciML) | Formal Verification (Lean 4)
I operate at the intersection of deep learning theory, formal mathematics, and computational urbanism. My research focuses on resolving the "black box" paradox in AI by architecting mathematically rigorous, interpretable, and machine-verified neural networks.
Rather than relying solely on empirical benchmarks, I utilize Lean 4 and Mathlib to formally verify optimization landscapes, gradient safety, and topological constraints in novel architectures.
My current work spans interpretable function approximation, continuous-time sequence modeling, and forensic spatial analytics:
- ๐งฎ Dictionary-KAN (DKAN): Resolving the optimization paradox of Kolmogorov-Arnold Networks. Lifts topology into the complex plane (Complex RKHS), utilizes Discrete Hierarchical Refinement (DHR) for zero-forgetting growth, and features machine-verified proofs of strict convexity and normal equations in Lean 4.
- ๐ Mamba-$\nabla$ (WIP): Resolving the "Mamba-3 Sparsity Paradox." Introduces the Polynomial Trapezoidal Rule for gradient-safe SSMs, Elastic State Partitioning (ESP) with Sinkhorn routing, and Asynchronous Latent Dreaming for closed-loop Model Predictive Control (MPC).
- ๐ Spectral Basis Interpretable Unit (SBIU): A quantum-inspired, classically verified orthogonal projection module. Maps scalars to probability distributions over learned Fourier bases for unsupervised physiological regime discovery (EEG/ECG).
- ๐๏ธ The Glass Box Planner: A normative framework for Urban AI. Shifts municipal algorithms from opaque "Inductive Scouts" to "Deductive Forensic Audits," validated via a 102k+ record spatio-temporal audit using Mamba-2 SSMs and custom Persian NLP.
Formal Methods & Mathematics
Lean 4 Mathlib Functional Analysis Complex Manifolds RKHS Lie Algebras (SO(d))
Deep Learning & SciML
PyTorch State-Space Models (Mamba) Kolmogorov-Arnold Networks Triton JAX ODE/PDE Discovery
Spatial Data Science & NLP
GeoPandas Spatial Econometrics Hazm (Persian NLP) LDA Zero-Inflated Poisson Forecasting
Systems & MLOps
Docker Next.js PostgreSQL Qdrant Neo4j Apache Parquet
- ๐ฅ Gold Medal, Star of United States, Silicon Valley (IWA 2025): For Simva, a low-resource, state-of-the-art Persian AI voice synthesis architecture.
- ๐ฅ Gold Medal, E-NNOVATE International Innovation Summit (2025): For CALLAI, an NLP-driven CRM tool optimizing civilian customer service workflows.
I am actively seeking research fellowships, deep-tech R&D roles, or PhD opportunities with teams pushing the boundaries of SciML, formal methods in AI, and algorithmic accountability.
- Email: kiarash7.mohammadi@gmail.com
- LinkedIn: linkedin.com/in/kiarash-mohammadi
- ORCID: 0009-0001-8760-977X
"I don't just train models; I formally verify their loss landscapes."



