Navin Dutta

Yang-Mills Mass Gap: Exploratory Lean 4 Formalization - CORRECTED (Problem Remains Open)

⚠ CORRECTION NOTICE - Version 1 claims retracted. See RETRACTION_NOTICE.md in this archive. Version 1 incorrectly claimed to have solved the Yang-Mills Mass Gap Millennium Prize Problem. Those claims are retracted in full. What was incorrect: The Lean 4 files contain open sorry p...

A Modular Formalization of 2D Navier-Stokes Uniqueness in Lean 4: Sorry-Free 1D Gagliardo-Nirenberg and Axiomatic Reduction of the Ladyzhenskaya Argument

Abstract: We present a machine-checked modular formalization in Lean 4 (with Mathlib4) towards the formal verification of the 2D incompressible Navier-Stokes global uniqueness theorem. The package delivers two primary contributions: (1) A complete, 100% sorry-free formal proof of...

Bistability and Bifurcation in Chaperone-Mediated Autophagy: A Mathematical Framework for Parkinson's Disease Therapeutics (PATO v1.0)

Background: Chaperone-mediated autophagy (CMA) failure is a central mechanism in Parkinson's disease (PD), driven by a positive feedback loop in which α-synuclein (αSyn) competitively inhibits LAMP2A — its own clearance receptor. Prior models have identified bistability in CMA-αS...