New Member: Feedback on Axiom + Sorry-Free Yang Mills

Stream: new members

[Jonathan Washburn]

Hi everyone,

I'm new here and outside academia, so I'm hoping for some guidance on sharing my work.

I've formalized a proof for the Yang-Mills existence and mass gap in Lean 4, reducing it to four primitive constants from an axiomatic framework I developed, called Recognition Science.

The repo is at https://github.com/jonwashburn/ym-proof - it's axiom and sorry-free, with 9,250 lines of code total (4,000 LoC in the foundational module for primitives).

The final theorem is in Stage6_MainTheorem/yang_mills_existence_and_mass_gap.lean:theorem yang_mills_existence_and_mass_gap : ∃ (H : HilbertSpace) (Φ : GaugeField H) (Δ : ℝ), is_pure_su3_ym H Φ ∧ has_mass_gap Δ ∧ Δ > 0 ∧ satisfies_axioms H ΦIt builds through layers for lattice gaps, OS reconstruction, continuum limits, and renormalization, with a bound in Renormalisation/RunningGap.lean: |Δ(1 GeV) − 1.10| < 0.06 GeV.

I'd appreciate any feedback or advice on next steps.

Thanks!
~Jon

[Eric Wieser]

Your code may be sorry free, but it is rejected by Lean; lake build YangMillsProof gives errors about things not existing

[Eric Wieser]

In general, your (multiple!?) lakefile(s) looks very non-standard which seems like a strong indication that they are AI generated and/or written in bad faith to hide the fact the code does not work

[Eric Wieser]

Which AI system(s) did you use here?

[Fred Rajasekaran]

Also on the math side things seem a bit shaky, for example the OS to Wightman axioms reconstruction is usually done via a type of analytic continuation, but

/-- Osterwalder-Schrader reconstruction theorem -/
theorem OS_to_Wightman (H : InfiniteVolume) (ax : OSAxioms H) :
  ∃ (W : WightmanTheory), True := by
  -- Construct Wightman theory from Euclidean data
  use {
    fields := []  -- Gauge-invariant field operators
    vacuum := { debits := 0, credits := 0, balanced := rfl,
                colour_charges := fun _ => 0, charge_constraint := by simp }
    poincare_covariant := trivial
    spectrum_positive := by
      intro p
      -- Energy-momentum relation
      simp
    local_commute := trivial
  }
  trivial

has no mention of it (nor of the semigroups that this analytic continuation is done with).

[Jonathan Washburn]

Hi Eric, thank you for taking a look!! I'm working on making these fixes right now. I've very new to all of this and just trying to complete some of these harder proofs as a proof of concept for my Recognition Science theory - but I don't want to pretend that I am something that I'm not.

It looks like I missed some duplicate lakefile's. Of course, I didn't write anything in bad faith, but you know how AI is always trying to make shortcuts. I apologize for code that looks like it's trying to hide something.

Primarily, I use Claude 4 Sonnet for bulk work, Opus for a little more challenging stuff, then o3-Pro to keep the others in check.

[Damiano Testa]

Also, you use native_decide: if your result ends up depending on the axiom Lean.ofReduceBool, it will be hard to distinguish that from sorry.

[Jonathan Washburn]

Hi Fred,

Gosh,

I must have put this more difficult one to the side and forgotten to come back to it.

I'll get it fixed now.I feel like it might be too big of an ask to request other examples of shaky math, but if you felt inclined to point some out, I'd really appreciate it. It would help me potentially identify a pattern of where I might have gone wrong, so I can look for similar areas myself and correct them.

I feel like I'm in a bit of an insecure spot here. I definitely do not want to put myself out here as something that I'm not. I somehow stumbled onto a science problem in quantum mechanics, and it just led me deeper and deeper.

For the last seven months, I've been working full time on developing a theory of everything type framework called Recognition Science.

I saw an opportunity to derive all of reality in Lean - which is my main project - but in doing so, it occurred to me that I might also bring a unique point of view to some of the harder math problems. If I could solve them in a more binary way - like with Lean - then that could lead to some exposure for my theory.

I'm not an academic - didn't graduate college or anything - so I'm very far outside of academia.

[Jonathan Washburn]

Thanks Damiano! I'm not sure if I should be replying with quote message, or there is an inline reply - I apologize again - very noob :P

[Jonathan Washburn]

I made some of the upates ! I made some of the suggested changes, but I'm falling asleep as I work. I'll return in the morning.

[A.]

Was it the AI that suggested using Lean?

[Jonathan Washburn]

A. said:

Was it the AI that suggested using Lean?

Yes. :)

[Michael Rothgang]

In case others search for this thread, e.g. in light of your ... interesting job posting: the current state of the repository still does not compile at all. I don't see how anything substantial is done here, and most likely it's looking-plausible-perhaps-at-a-distance-but-actually-not-working-at-all LLM output. As such, I won't engage further.

[Jonathan Washburn]

Michael Rothgang said:

In case others search for this thread, e.g. in light of your ... interesting job posting: the current state of the repository still does not compile at all. I don't see how anything substantial is done here, and most likely it's looking-plausible-perhaps-at-a-distance-but-actually-not-working-at-all LLM output. As such, I won't engage further.

Thanks for checking back on my proof (even if just for the last time :). I haven't replied in this thread because I've been trying since my last reply to dig myself out of the mess the proof was in. I think I'm getting close, but also... who knows.

My current plan is to get the repository as clean as I can. Then check back in.

[Eric Wieser]

I think I'm getting close, but also... who knows.

This is like thinking if you throw your rock just a little harder it will hit the moon. If you are serious about wanting to learn Lean, you should start by trying to formalize a well known true proof, so that you develop some intuition for when the Lean code says the right thing and when it doesn't.

[Jonathan Washburn]

Obviously that advice makes total sense and is logical. However, I am not here to learn Lean. I'm strictly mission driven to formalize reality in Lean - which I know sounds crazy.

So I'm here to find help and support, and share what I'm working on. I'd prefer to pay experts in Lean to help me on this, but I felt that I'd have to at least bootstrap some working models to be taken seriously in some regards. (Though it doesn't seem to be working very well ;) lol

[Arthur Paulino]

I think what makes people feel off in exchanges like this is that you're acting as a "man in the middle" in a mutual conversation between the community and the AI tool you're interacting with.

[Arthur Paulino]

If you're not interested in learning Lean, there's very limited space to even start helping you. Think about it...

[Jonathan Washburn]

Arthur, I get it - to a degree. I'm responding on my own. These aren't Chatgpt responses.

I am "learning" Lean, I'm just doing it in a way that utilizes AI as a tool. It's the same argument that's been had on every new invention - calculators, computers, etc.

The caveat here is that my end goal isn't coding Lean, but to solve a specific real world problem or set of real world problems, using Lean. And, I want to use all resources available to do that - including, other experts if possible.

I'm a tech entrepreneur - for 30 years now. This doesn't feel any different to me from learning the very basics of HTML when browsers first came out, so that I could build a (shitty) webpage, and then finding engineers to actually build the real thing.

I guess the question is "why am I here".

[Jonathan Washburn]

Arthur Paulino said:

I think what makes people feel off in exchanges like this is that you're acting as a "man in the middle" in a mutual conversation between the community and the AI tool you're interacting with.

Also, I'm listening very intently to all of the advice and critique that I'm getting, and I'm working to correct it as quickly as I can. The truth is that I am human and limited. I'm trying to do the best with the tools that I have, and I'm not pretending to be something that I'm not.

[Arthur Paulino]

Coding in language X, for whatever X, rarely is the end goal of any sane project that involves coding.

You can start with the basics, installing the software and creating a project from scratch so you can work upwards.

[Arthur Paulino]

The best way I've found so far to use AI with Lean is to do it very lightly. Get your definitions and theorem statements right very meticulously in your IDE and then ask for assistance when proving.

[Jonathan Washburn]

Arthur Paulino said:

Coding in language X, for whatever X, rarely is the end goal of any sane project that involves coding.

You can start with the basics, installing the software and creating a project from scratch so you can work upwards.

I actually have 10 strong engineers on my team, and I could have asked them to do this task, but I did want to tackle and understand it on my own. Which I feel, I have.

The project I'm working on is crazy, and even asking people that I employ to work on it, feels like a big ask for me. So I did it myself. What I have I am proud of. I think its a very strong start.

[(deleted)]

But... if you don't have a good mental model of how Lean works... how can AI help you? And it's been shown over and over that AI isn't that good at Lean. That excitement over Claude using MCP to write Lean code is over. Even reinforcement learning Lean LLMs (DeepSeek Prover, Kimina Prover) struggle with the most basic problems. Using AI can enhance our productivity if we are aware of the limitations.

[(deleted)]

My literal job is training AIs to write Lean code.