I build things that don't usually sit next to each other.
A Lean 4 formalization of the Riemann Hypothesis. An album. Two books. AI products for style, education and reentry. A licensed trucking company in New York. And reentry work, since 2013, that helps people find their way back.
None of it came through the usual path. I built a logistics company, then invested its capital in teaching myself to build with AI, and used it to take on some of the hardest problems I could find.
What ties it together is one belief: confidence and uncertainty, choice and limits, persistence and resistance turn an idea into something real.
Select a section to view its full page.
Riemann Hypothesis: A Lean 4 Formalization
Lean 4 formalization made public May 30, 2026 on GitHub · Archived on Zenodo August 15, 2026
Travis Darshan's single-author formal research project on the Riemann Hypothesis — one of mathematics' great unsolved problems, open since 1859. Rather than relying only on a traditional proof on paper, it's built in Lean 4, software that checks every logical step by machine. His compiled library runs to over 125,000 lines of Lean across more than 2,700 verified theorem/lemma declarations, and its central result is a machine-verified conditional theorem whose endpoint is the full Riemann Hypothesis — archived with a citable DOI. Establishing the final, unconditional step is the open research frontier the project is working toward now.
Travis Darshan's Lean 4 verification output shows that the certified result builds with no sorry or admit placeholders and no custom axioms. In Lean, a sorry is a placeholder for a step you haven't actually proved — it tells the system to assume the result and move on, so even one buried anywhere leaves a gap in the proof. Having no sorry means nothing in the compiled formalization is skipped with an unfinished proof placeholder; combined with the absence of custom axioms, the certified result rests only on Lean's standard logical foundation. Anyone can re-run the repository's exact verification commands and check the result independently. As of now, Travis Darshan's certified Lean 4 formalization compiles with no sorry.
Yang–Mills: A Lean 4 Formalization
Lean 4 formalization begun August 2026 on GitHub · Archived on Zenodo October 9, 2026
A single-author Lean 4 project on Yang–Mills theory, the gauge theory behind the strong and weak nuclear forces. It’s connected to one of the Clay Millennium Prize Problems, Yang–Mills existence and mass gap. The project formalizes twisted SU(2) cell geometry and the nonlinear Wilson action. Its central result is a machine-verified directional quadratic limit connecting the action to the cell’s physical projection. This finite-cell result is a step toward the larger research program; continuum existence and a mass gap remain open.
The repository documents verification with no sorry dependencies or custom axioms for its certified results, and provides commands so anyone can re-run the verification.
Magnifica Humanitas: A Lean 4 Analysis of AI-Governance Commitments
Release 1.1 · November 2026 · Archived on Zenodo
A formal study of selected AI-governance commitments in Pope Leo XIV's encyclical Magnifica Humanitas (§§97–111). Through close reading and examples checked in Lean 4, it distinguishes a stated protection from the powers and actions needed to make it effective: an accessible appeal, a reviewer with authority, and a correction that actually reaches the decision.
Album
Man with the Phoenix Tattoo by Travis Darshan — streaming now.
Don't Leave Me (lead single) — streaming now on Spotify and Apple Music.
Books
Published works by Travis Darshan spanning fiction, personal reflection, and ideas about human potential, resilience, and change.
Paradoxically A Woman — by T. Darshan
The Prisoner's Stone — by Travis Darshan
Tristan's Pick
Tristan's Pick was originally a custom GPT created on OpenAI's launch day, November 6, 2023. Part of the first wave of custom GPTs introduced that day, it later went on to reach #1 in the Fashion category. Today, the concept has grown into a new and updated Tristan's Pick web app — a multidimensional, interactive style and venue experience.
Upload a photo and a few pieces from your closet, and Tristan's Pick builds a personalized digital version of you — then styles complete looks on you: outfit, shoes, jewelry, and accessories, matched to wherever you're headed, from Carbone to a rooftop bar in Cartagena. Don't love the look? Ask for another, and Tristan will search the web for what your closet is missing. Tristan's Pick reads how a room dresses and when it peaks, rates looks for confidence and impact, and learns your taste as you go.
Beyond the Curve
Founded in 2013, Beyond the Curve helps people coming home from incarceration find their footing — bringing housing, ID and documents, employment, benefits, health care, legal aid, and family support into one place, right when it's needed most. It pairs a Reentry Companion that answers real questions with a Justice Advocate that turns reporting and public records into reviewed commentary on reentry and justice.
Advocacy
Travis Darshan has also brought his advocacy into public conversations, including a radio broadcast at Vassar College addressing incarceration, reentry, second chances, and rebuilding after release.
College Admission Pathfinder
A free, AI-powered college-admissions counselor giving every student — whatever their income or background — the expert guidance families usually pay thousands for: GPA, essays, scholarships, financial aid, and application strategy. Travis Darshan co-founded it and built the AI as Chief AI Architect. It runs as a custom GPT with a companion website and app.
Darshan Enterprises
Founded 2019 · New York · Logistics → AI
Darshan Enterprises began as a licensed trucking and logistics company in New York, moving import and export freight for forwarders at JFK Airport, along with intrastate and interstate freight. Its capital funded three years of independent AI research. Operations are paused; today it is the umbrella for my work in AI.