Projects

AI-Assisted Mathematics

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

PALOMAR-verified core · ongoing manuscript development

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. The current manuscript is being reorganized around the broader factorial-residue hypergraph and covering-congruence theory.

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
  • Working draft (human exposition and revision in progress)

PALOMAR-verified core · ongoing manuscript development

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
  • Human mentor: Professor Kyungyong Lee, who aided me in the process of verification
  • Working draft (human exposition and revision in progress)

PALOMAR-verified core · ongoing manuscript development

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: heavily 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
  • Working draft (human exposition and revision in progress)

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