Projects

AI-Assisted Mathematics

Lean-verified results and ongoing AI-assisted mathematical research.

PALOMAR-verified core · no separate human exposition planned

A weighted prime-coloured hypergraph framework for factorial residues, in which compatible residue covers correspond exactly to Chinese-remainder covering systems. The main structural result gives a fixed proportional saving in the minimum compatible covering cost,

\[\kappa(L)\le (1-\delta)L\log L\]

for all sufficiently large \(L\).

As an arithmetic application, the framework gives a quantitative resolution of an auxiliary factorial problem posed by Erdős: for every sufficiently large \(L\), there are quantitatively many \(L\)-rough integers

\[2L!<n\le (L+1)!\]

such that \(n-k!\) is composite for every \(1\le k\le L\).

The formally verified version of the auxiliary theorem is registered as PALOMAR-2026-08-27-000003 v1.

PALOMAR GitHub

  • Discovery and proof development: mostly AI-assisted using ChatGPT Web (GPT-5.6 Sol Pro), Codex (GPT-5.6 Sol Max), and Aristotle (Harmonic). Human involvement consisted of selecting and reframing the problem, proposing the broader factorial-residue hypergraph interpretation, and reviewing the resulting arguments
  • Formal verification: Lean 4 · Comparator · Lean kernel · NanoDa
  • Verified scope: quantitative auxiliary Erdős theorem and its problem-specific proof chain
  • Why this problem: a secondary open problem I chose during RIPS; the primary one was the Tunnell map below. I wanted a question with a short elementary statement that could be checked in Lean. Erdős’s auxiliary factorial question fit that; the factorial-residue hypergraph framing was the part I added
  • Human exposition: none planned, since a stronger result has since appeared and this one does not add much

PALOMAR-verified core

A deterministic arithmetic-combinatorial framework for Tunnell’s ternary quadratic forms, in which the numerical \(2{:}1\) relation between two representation sets is realized by an explicit map. Writing

\[\mathcal{B}_n=\left\{(x,y,z)\in\mathbb{Z}^3:2x^2+y^2+8z^2=n\right\},\qquad \mathcal{A}_n=\left\{(u,v,w)\in\mathbb{Z}^3:2u^2+v^2+32w^2=n\right\},\]

the main result constructs, for every odd positive squarefree \(n\) satisfying \(|\mathcal{B}_n|=2|\mathcal{A}_n|\), a deterministic map

\[\Phi_n:\mathcal{B}_n\longrightarrow\mathcal{A}_n,\qquad \left|\Phi_n^{-1}(a)\right|=2 \quad\text{for every }a\in\mathcal{A}_n.\]

For odd squarefree congruent numbers, Tunnell’s theorem supplies the required counting identity. The construction combines an elementary even-coordinate map, three explicit quarter-turn correspondences, and a canonical stable matching of the remaining antipodal orbits determined by primitive midpoint directions.

The executable two-to-one map and its registered specifications are formally verified and registered as PALOMAR-2026-09-07-000010 v2.

PALOMAR GitHub

  • Discovery and proof development: AI-assisted using ChatGPT Web (GPT-5.6 Sol Pro), Codex (GPT-5.6 Sol Max), and Aristotle (Harmonic), with human direction in preventing dead ends and guiding the argument
  • Formal verification: Lean 4 · Mathlib · Comparator · Lean kernel · NanoDa
  • Verified scope: deterministic global map, inverse identities, exactly-two fibre theorem, and the complete \(n=41\) example
  • Why this problem: this was the primary problem my professor gave me during RIPS. It is not open in the usual sense as Tunnell’s theorem already gives the counting identity. What we wanted was a constructive map. As this had elementary statement, a combinatorial flavor and a constructive proof which would also let me see how good the LLM is regarding non counterexample Maths (if that makes sense)
  • Human mentor: Professor Kyungyong Lee, who aided me in the process of verification

PALOMAR-verified core

A global solution for the classical Moh \(P_3\) curve, arising from the family introduced by T. T. Moh in 1974 (Moh).

Let \[\mathfrak{p}=\ker\!\left(\mathbb{Q}[x,y,z]\to\mathbb{Q}[t]\right),\qquad (x,y,z)\mapsto(t^6+t^{31},t^8,t^{10}).\] The main result constructs two explicit degree-\(16\) polynomials \(H_1,H_2\in\mathbb{Q}[x,y,z]\) satisfying \[\mathfrak{p}^2\subseteq(H_1,H_2)\subseteq\mathfrak{p}.\] Hence \[\sqrt{(H_1,H_2)}=\mathfrak{p},\] so the entire affine Moh curve is cut out set-theoretically by two polynomial equations.

The construction uses a globally invertible transformation of the Hilbert–Burch matrix into a symmetric form, followed by determinant and adjugate identities. The final verification reduces to a finite collection of exact polynomial identities: two proving \(H_1,H_2\in\mathfrak{p}\), and ten proving \(\mathfrak{p}^2\subseteq(H_1,H_2)\).

The set-theoretic complete intersection and its registered specifications are formally verified and registered as PALOMAR-2026-09-07-000012 v1.

PALOMAR GitHub

  • Discovery and proof development: AI-assisted using ChatGPT Web (GPT-5.6 Sol Pro and GPT-6 Pro)
  • Explicit witnesses: two degree-\(16\) polynomials \(H_1,H_2\)
  • Exact verification: 12 explicit polynomial identities over \(\mathbb{Q}\)
  • Formal verification: Lean 4 · Mathlib · Comparator · Lean kernel · NanoDa
  • Macaulay2: independent replay script prepared; external execution pending
  • Why this problem: during my Algebraic D-modules course I had planned Hartshorne’s quartic as a semester project. While reading, I encountered this smaller problem in Clare D’Cruz’s paper, Symbolic Powers, Set-Theoretic Complete Intersection and Certain Invariants, and used it as a test: if AI could not solve it with minimal guidance, I would take it as the project; otherwise I would return to Hartshorne. It solved with minimal guidance, so it is not my semester project

Class and Research Projects

SIHR Model Visualization

2025

An interactive visualization tool for analyzing SIHR-IPC (Susceptible-Infected-Hospitalized-Recovered with Individual Possion Clock) epidemiological models.

Mathematical Model

The SIHR-IPC model is described by the following system of ordinary differential equations:

\[\frac{ds}{dt} = -p_{SI}\beta si\]

\[\frac{di}{dt} = p_{SI}\beta si - \gamma(1-p_{II})i\]

\[\frac{dh}{dt} = p_{IH}\gamma i - p_{HR}\alpha h\]

\[\frac{dr}{dt} = p_{IR}\gamma i + p_{HR}\alpha h\]

where:

  • \(s\): Susceptible proportion
  • \(i\): Infected proportion
  • \(h\): Hospitalized proportion
  • \(r\): Recovered proportion
  • \(\beta\): Transmission rate
  • \(\gamma\): I outflow rate
  • \(\alpha\): H outflow rate
  • \(p_{SI}\): Probability of S→I transition
  • \(p_{II}, p_{IH}, p_{IR}\): I outflow probabilities (sum = 1)
  • \(p_{HR}, p_{HH}\): H outflow probabilities (sum = 1)

Key threshold parameters:

  • \(\sigma = \frac{p_{SI}\beta s_0}{\gamma(1-p_{II})}\): Basic reproduction number
  • \(\tilde{\sigma} = \frac{\gamma p_{IH} i_0}{\alpha p_{HR} h_0}\): Initial condition ratio
  • \(\tilde{\tilde{\sigma}} = \frac{\gamma p_{IH} i_{peak}}{\alpha p_{HR} h(t_{pi})}\): Peak condition ratio

View Demo

SIHRS Model Visualization

2025

An advanced interactive visualization tool for analyzing SIHRS (Susceptible-Infected-Hospitalized-Recovered with Death) epidemiological models with reinfection dynamics and mortality tracking.

The MATLAB code for SIHRS can be found at https://github.com/GrgAakash/Code-collection--REU-25/tree/main/SIHRS

Mathematical Model

The SIHRS model is described by the following system of ordinary differential equations:

\[\frac{ds}{dt} = -\beta p_{SI} si + p_{RS}\lambda r\]

\[\frac{di}{dt} = \beta p_{SI} si - \gamma(1-p_{II})i\]

\[\frac{dh}{dt} = p_{IH}\gamma i - \alpha(1-p_{HH})h\]

\[\frac{dr}{dt} = p_{IR}\gamma i + p_{HR}\alpha h - p_{RS}\lambda r\]

\[\frac{dd}{dt} = p_{ID}\gamma i + p_{HD}\alpha h\]

where:

  • \(s\): Susceptible proportion
  • \(i\): Infected proportion
  • \(h\): Hospitalized proportion
  • \(r\): Recovered proportion
  • \(d\): Death proportion
  • \(\beta\): Transmission rate
  • \(\gamma\): I outflow rate
  • \(\alpha\): H outflow rate
  • \(\lambda\): R outflow rate (reinfection)
  • \(p_{SI}\): Probability of S→I transition
  • \(p_{II}, p_{IH}, p_{IR}, p_{ID}\): I outflow probabilities (sum = 1)
  • \(p_{HH}, p_{HR}, p_{HD}\): H outflow probabilities (sum = 1)
  • \(p_{RR}, p_{RS}\): R outflow probabilities (sum = 1)

View SIHRS Demo

Q,T-Catalan Chain Decompositions

2025

An advanced interactive tool for exploring Q,T-Catalan chain decompositions through NU₁, NU₂, ND₁, and ND₂ maps, including NU₁-tails, NU₂-bridging, and global chain construction.

Explore Q,T-Catalan Chains   Dyck Path Visualizer   HLLL verification tools