I'm an MBA-Tech (AI/ML) student at D.Y. Patil University, Navi Mumbai. I work on projects that sit between mathematics, formal logic, machine learning, and systems software.
I like taking a complicated system apart until I can identify the primitive that matters — a Boolean expression, a matrix solve, a Fourier component, or a recurrence. From there, I build a working implementation, state what should be true, and test the result against evidence rather than intuition.
That usually means one of two things: proving an invariant in Lean 4, or designing an experiment that is strong enough to expose where an implementation fails.
Currently exploring:
- Formal verification for machine-learning systems, optimizers, and cryptographic constructions
- Better methods for deep learning
- Provenance and watermarking for generated media
- Computability, self-reference, and the foundations of formal systems
| 🔍 Deconstruct | 📐 Formalize | ⚙️ Build | ✅ Validate |
|---|---|---|---|
| Find the actual primitives and assumptions | State the claim precisely, often as Lean 4 theorems | Implement the reference system before optimizing it | Measure it, attack it, or prove where it holds |
I care about the result, but also about the boundary of the result: what was measured, what was proved, what was assumed, and what still needs work.
These are the projects I keep returning to: some are research implementations, some are formal experiments, and some are small systems built to make an idea tangible.
- Conjugate State Machines — A research implementation of recurrent fast-weight memory. CSMs use a key-correlation solve rather than a plain Hebbian read, with PyTorch, Triton, C++/HIP kernels, matched baselines, and Lean 4 theory definitions.
- RootFree-Shampoo — The official implementation of RootFree-Shampoo (RFS), an experimental optimizer.
- STAM — Certified, budget-aware loss-landscape visualization for PyTorch models. It uses second-order Taylor patches on a two-dimensional plane and reports an error estimate for each figure.
- Kenian — Trajectory-sliced third-order optimizers for deep learning, with CUDA, Triton, and formal-verification experiments.
- Melodic Intelligence Layer — A mathematical theory of algorithmic piano composition with musical identity, built without neural networks and supported by Lean 4 proofs.
- SIGIL — A stratified watermark for generated images that combines analytic invariants, learned robustness, and Lean-verified statistical guarantees.
- VIOLET — A Python electromechanical cipher-machine simulator with a desktop app, empirical theorem tests, and statistical cryptanalysis tools.
- HMV — An experimental 1536-bit sponge hash family with a controller-driven permutation and machine-checked Lean 4 wide-trail proofs.
- DCS-PCS — Code and empirical artifacts for the Diagonal Constraint Structure and Practically Complete System: a study of self-reference, impossibility, and grounded completeness.
- K-Map Tic-Tac-Toe — A Tic-Tac-Toe AI powered by Karnaugh maps and Boolean logic rather than game-tree search.
- Expression Tree Visualizer — An interactive desktop tool for converting infix expressions, building expression trees, and stepping through parsing, traversal, and evaluation.
"Innovation isn't just about making new things; it's about forcing cross-domain analogies to see what sparks."
Thanks for stopping by — if something here sparks an idea, feel free to explore the repositories or say hello. Built with curiosity, and more proofs than strictly necessary.