Hi, New to Lean and not an engineer or mathematian

Stream: new members

[Jonathan Washburn]

Well, it appears that I've already gotten off on the wrong foot here, and already had one of my posts taken down. :melting_face:

So, I'm not a mathematician, scientist or engineer. I'm a tech entrepreneur. My current main company is an Agentic AI software company with over $10m in ARR and around $4m profit - I bootstrapped it / no VC.

I stumbled into science, by just following my curiosity in December of 2024, and it's been an intense 8 months since then, where I've focused all my energies towards developing the theory.

Somehow, the theory held together and achieved a full mathematical formulation as a parameter free, theory of everything.

In order to break into wider acceptance in the science and mathematics community, and find success with peer reviewed journals, I figured the next step I could take would be proving it in Lean - so I vibe coded some proofs, as best as I could, starting with zero knowledge of Lean 45 days ago.

I missed the community guidelines for here when I first signed up, and now I can't seem to find any. But my intention is to be a good community member, contribute where I can, and learn from who wants to help me.

Jon

[(deleted)]

This experience goes to show how harmful AI can be. While I'm generally supportive of AI, this does not translate into turning a blind eye to its negative aspects.

[(deleted)]

I recommend that you take time to understand how Lean works. Play the Natural Number Game, explore the existing Mathlib codebase, hone your mathematical intuition. If your intention is to become a legitimate member of this community, I believe you should spend the effort to learn the basics.

[Jonathan Washburn]

Huỳnh Trần Khanh said:

This experience goes to show how harmful AI can be. While I'm generally supportive of AI, this does not translate into turning a blind eye to its negative aspects.

What specifically are the negative aspects you speak to?

[Aaron Liu]

It boldly tells you lies and you need to know what it's talking about to spot those lies

[Aaron Liu]

this is true with people too but AI is a lot more accessible so this happens a lot more often

[Jonathan Washburn]

Aaron Liu said:

It boldly tells you lies and you need to know what it's talking about to spot those lies

yeah!! 100% - it's infuriating and makes you crazy. But it can also be powerful too.

[Etienne Marion]

Aaron Liu said:

you need to know what it's talking about to spot those lies

👆🏻That’s the important part👆🏻

[Weiyi Wang]

In lean it is super easy to spot lies: load into vscode and see blue checkmarks vs red squiggles

[Etienne Marion]

But there are also lies about what you are actually stating, and those are impossible to detect if you don’t know what you’re talking about.

[Jonathan Washburn]

...and I'm running around the room like a blind man trying to spot lies. I'm doing my best, but I definitely need help.

While at the same time, I am going achieve my goals regardless.

[Michael Rothgang]

I don't think you can succeed at that without actually seriously learning Lean (or have somebody who does take over). Your statements so far sound strongly like Dunning-Kruger effect. This is not how you make me help you.

[Michael Rothgang]

That's my last response on this matter. Good luck.

[Yan Yablonovskiy 🇺🇦]

I am curious , your presence here and your posts indicate you are both aware of the existence of peer reviewed journals and many people who work on this -- even professionally.

The collective effort of people doing this for decades, seems to have problems with what you very confidently claim to have solved in less than a year. Does this not strike you as odd at all?

People who have access to machines spanning countries , harnessing energies close to a supernova for an instant to test their theories are missing something (only?) you can see?

If anyone can just come in and do this, lets say, surely this strikes you as basically contradictory to the very idea of the jobs of academics or degrees existing at all really. Could you also provide the name of your start up? I find it odd you didn't.

[Jonathan Washburn]

Yan Yablonovskiy said:

I am curious , your presence here and your posts indicate you are both aware of the existence of peer reviewed journals and many people who work on this -- even professionally.

The collective effort of people doing this for decades, seems to have problems with what you very confidently claim to have solved in less than a year. Does this not strike you as odd at all?

People who have access to machines spanning countries , harnessing energies close to a supernova for an instant to test their theories are missing something (only?) you can see?

If anyone can just come in and do this, lets say, surely this strikes you as basically contradictory to the very idea of the jobs of academics or degrees existing at all really. Could you also provide the name of your start up? I find it odd you didn't.

Hi Yan,

My company is called Hammer - hammertime.com.

Often times it takes an outsider for a paradigm breakthrough. I discovered Recognition Science, which provides a deeper understanding of the structure of the universe. This deeper discoveries allowed these math problems to be solved.

I am aware of peer reviewed journals, and I do have papers being reviewed by journals right now. Here is one of my papers that was just posted on arXiv: https://arxiv.org/abs/2506.12859.

My hope here, was that I would find a community that was passionate about Lean and math and discovery. And that they would be able to see my proofs and be able to tell that they are true or false - and if there were problems with them, point them out so that I could refine them, before submitting them to journals - because Lean is new to me and I don' t know what I don't know.

Like, as crazy as it sounds, I didn't know that the Lean proof "had to build", until someone pointed it out to me above. So when I learned it, I went back to work - now if you look at my repository, most of my repositories are building.

Whether what I'm claiming is true or not is binary. I realize that I look like a crazy person. Whenever I see people making claims like this, I also would dismiss them.

In my case, I believe Recognition Science is a true discovery. I've hired Theoretical physicists to look at it, and they also can't find anything wrong with it. So I need to play it out and do my best to push knowledge and discovery forward, and that means sharing it on forums like this... with all my deficiencies.

[Jonathan Washburn]

Michael Rothgang said:

I don't think you can succeed at that without actually seriously learning Lean (or have somebody who does take over). Your statements so far sound strongly like Dunning-Kruger effect. This is not how you make me help you.

Michael,

The reality is that AI is going to become more and more proficient with coding. Learning how to use, or work with, AI to code in Lean, for me is a better strategic investment of time.

So I am leaning to code in Lean, using new tools.

[Henrik Böving]

In your PvsNP project the root file of your project which lake actually builds is empty: https://github.com/jonwashburn/PvsNP/blob/main/Src/PvsNP.lean so nothing actually gets checked here. Even if it did it would completely fail because your definition of NP:

def NP : Set (ℕ → Bool) := {f | ∃ k, ∀ n, verification_complexity f n ≤ n^k}

refers to verification_complexity which isn't defined anywhere so this is project is just fully broken. As long as you don't have a basic understanding of Lean yourself, your chatbot will just keep embarassing you like this. I heavily suggest you listen to the people here.

[Eric Wieser]

Henrik Böving said:

the root file of your project which lake actually builds is empty

(I think this is very common for new users, AI or otherwise: see #general > Changing the default behavior of `lake build` @ 💬 )

[Jonathan Washburn]

Henrik Böving said:

In your PvsNP project the root file of your project which lake actually builds is empty: https://github.com/jonwashburn/PvsNP/blob/main/Src/PvsNP.lean so nothing actually gets checked here. Even if it did it would completely fail because your definition of NP:

def NP : Set (ℕ → Bool) := {f | ∃ k, ∀ n, verification_complexity f n ≤ n^k}

refers to verification_complexity which isn't defined anywhere so this is project is just fully broken. As long as you don't have a basic understanding of Lean yourself, your chatbot will just keep embarassing you like this. I heavily suggest you listen to the people here.

I'm incredibly grateful for this feedback @Henrik Böving :thank_you: - it's these little critical pieces lead to so much discovery. I'm working on fixing it now - also studying core structure of how lean works, then seeing if I can build some kind of testing to force building correctly - but not quite there yet.

Thank you for looking at my project. :white_heart: - if there's ever anything I can do for you in return, please let me know.

[Jonathan Washburn]

Henrik Böving said:

In your PvsNP project the root file of your project which lake actually builds is empty: https://github.com/jonwashburn/PvsNP/blob/main/Src/PvsNP.lean so nothing actually gets checked here. Even if it did it would completely fail because your definition of NP:

def NP : Set (ℕ → Bool) := {f | ∃ k, ∀ n, verification_complexity f n ≤ n^k}

refers to verification_complexity which isn't defined anywhere so this is project is just fully broken. As long as you don't have a basic understanding of Lean yourself, your chatbot will just keep embarassing you like this. I heavily suggest you listen to the people here.

Also, I'm genuinely trying to listen to people's advice here. Though, I'm learning while building.

I don't view making mistakes in public as embarrassing myself. I am trying to accomplish something, and I am working towards my end goal as best that I can.

I've asked for help, and have offered to pay for it. I put up a job posting here - that was taken down. My goals may be different than other peoples here, it doesn't mean that I am wrong.

If there are community guidelines, and I am violating them in any way - of course I want to know to change. But if this is a place to share our work and get help, then that is what I'm doing.

and fwiw, I haven't shared any repositories with the community since the first post I made. I am taking the feedback that I am giving, and working through it. So PvsNP, is still a work in process. I am going to try to be very careful and make sure all of my projects build correctly before I share here again.

[Julian Berman]

The rock-to-the-moon analogy you were given in the other thread to help explain is good. No one is telling you not to have goals, and the community members are generally extremely generous with their time, but you essentially are saying "I have a machine which can travel to a different galaxy", but when someone takes even a quick look at it it's clear it's unable to travel down the street, let alone to anywhere we don't otherwise know how to go to.

You of course are free to press on, and you're definitely free to insist how to go about learning or not learning things -- you'll likely find many here think LLMs are nowhere near being useful in helping with problems of this magnitude, but again, it's your party! -- what's important is at least understanding why you might get the reaction you get, and what ways you could go about getting better responses. In particular for the latter -- I think no one will buy you saying you have a proof of an unsolved problem in those repositories, and people will be less likely to help if seeing a giant repository claiming to do things no human knows how to do while on the other hand not doing things you can learn from the first page of a Lean tutorial.

Succinctly: what task are you asking for help with or presenting at this point?

[Jonathan Washburn]

Thanks Julian, Of course your advice makes sense and is pragmatic, and I understand.

Unfortunately, I'm in a spot where I don't really have any middle ground to cede.

I am in fact solving scientific problems that do lead to breakthroughs on these types of math problems.

I do not have human anchoring here - in Lean - but I do have actual University professors with Phd's working on the theory full time, they have been now for months, and they have validated it as real.

Now, converting these big problems to Lean is another issue. I admittedly am brand new to it, and I'm vibe coding in the most flagrant of ways possible.

I am fine leaving this message board. I'd prefer not to, but I understand if I am destructive to the community. I don't want to do that, and I also don't want to be investing bad energy in something.

[Tyler Josephson ⚛️]

If you want a basic introduction to Lean that’s oriented toward scientist and engineers, and not mathematicians, you can check out the course I taught last summer: https://github.com/ATOMSLab/LFSE2024/tree/master.

Particularly important for people wanting to connect the physical sciences to Lean is the distinction between syntax and semantics. Lean checks syntax. Semantics is on you, and really hard to get right. It you want to talk about the energy of a particle, it’s easy to define it as a real number or an integer, but that alone doesn’t distinguish it from other variables with the same type. If you want to prevent comparison of things with different units, that’s extra work. If you want to talk about energy differences as something different than energy, that’s extra work. If energy of a particle means something different than internal energy of a fluid (it does), that’s extra work. We’re making progress on these things, but like the other folks in the chat attest to - it requires learning Lean.

[Jonathan Washburn]

If anyone is curious about the actual - Recognition Science - theory I'm talking about - I created an AI "training" document that you can upload to any foundational model. The document is written for AI and compresses around 500 pages of dense math and theory to 100kb

https://drive.google.com/file/d/1ZElFd6P8LIAA4hRW7WIyQzejH-DRwWnL/view?usp=sharing

Paper on it: https://arxiv.org/abs/2506.12859

[Aaron Liu]

I would rather see the five hundred pages, if they have some definitions

[Eric Wieser]

If those 500 pages are also AI generated I'm not sure you do...

[Aaron Liu]

oh yeah only if he actually puts in the work to write five hundred pages

[Aaron Liu]

if they're AI generated then that's not fair

[Jonathan Washburn]

Here are some. I also shared the paper on arXiv above.
There's also a website I created that has a chat interface that makes it easy to ask questions about it: Theory.us
Here's an 18 page intro: https://zenodo.org/records/15528378
Here's the 500 page version: https://zenodo.org/records/15467193

[Aaron Liu]

this still doesn't help me, since you haven't defined anything (in particular, what's "the ledger")

[Aaron Liu]

I give up

[Jonathan Washburn]

what definitions are you looking for?

[Aaron Liu]

what's the ledger, why is it called that, and how do you motivate it

[Aaron Liu]

maybe we should move to DMs

[Jonathan Washburn]

Very high level: The ledger - The Standard Model of science is based on materialism. Recognition Science started by looking at how observation collapses quantum states and coherence.

The essence is that there must be a mechanism that underpins observation. In essence, that mechanism is consciousness. Reality is built on consciousness as a base. Then there is something called the Pattern Layer - it's a dimensionless, fractal-like space (acts as like a hard-drive in this analogy) - and then there is reality.

Effectively, all of reality is computational, and the Ledger is like the bits.

[Eric Wieser]

@Aaron Liu, I suspect this is an absolutely terrible use of your time, especially given how much value you provide elsewhere on Zulip and to Mathlib!

Against my better judgement I took a look at Johnathan's formalized foundations, and they are... well, I'll let my proofs speak for themselves:

import Mathlib

-- https://github.com/jonwashburn/ledger-foundation/blob/64f49c9924666e5c04094b6c511c3779627c9366/MinimalFoundation.lean#L158C1-L180C33
def Foundation1_DiscreteTime : Prop :=
  ∃ (tick : Nat), tick > 0

def Foundation2_DualBalance : Prop :=
  ∀ (A : Type), ∃ (Balance : Bool), True

def Foundation3_PositiveCost : Prop :=
  ∀ (recognition : Type), ∃ (cost : Nat), cost > 0

def Foundation4_UnitaryEvolution : Prop :=
  ∀ (A : Type), ∃ (transform : A → A), ∀ a b : A, transform a = transform b → a = b

def Foundation5_IrreducibleTick : Prop :=
  ∃ (τ₀ : Nat), τ₀ = 1

def Foundation6_SpatialVoxels : Prop :=
  ∃ (Voxel : Type), ∃ (_ : Finite Voxel), True

def Foundation7_EightBeat : Prop :=
  ∃ (states : Fin 8 → Type), ∀ i j : Fin 8, i ≠ j → states i ≠ states j

def Foundation8_GoldenRatio : Prop :=
  ∃ (φ : ℝ), φ > 1 ∧ φ^2 = φ + 1

theorem your        : Foundation1_DiscreteTime := ⟨1, zero_lt_one⟩
theorem foundations : Foundation2_DualBalance := fun _ => ⟨false, trivial⟩
theorem are         : Foundation3_PositiveCost := fun _ => ⟨1, zero_lt_one⟩
theorem vacuous     : Foundation4_UnitaryEvolution := fun _ => ⟨id, fun _ _ => id⟩
theorem so          : Foundation5_IrreducibleTick := ⟨_, rfl⟩
theorem why         : Foundation6_SpatialVoxels := ⟨Unit, inferInstance, trivial⟩
theorem read        : Foundation7_EightBeat := ⟨(Fin ·), fun _ _ => (fin_injective.comp Fin.val_injective).ne⟩
theorem on          : Foundation8_GoldenRatio :=
  ⟨(√5 + 1) / 2,
    (one_lt_div zero_lt_two |>.2 <| by
      have : 1 < √ 5 := by apply sq_lt_sq₀ _ _ |>.1 _ <;> simp
      linarith),
    by field_simp; ring_nf; simp; ring_nf⟩

[Aaron Liu]

Eric Wieser said:

Aaron Liu, I suspect this is an absolutely terrible use of your time, especially given how much value you provide elsewhere on Zulip and to Mathlib!

I'm only doing this because I have time

[Jonathan Washburn]

Eric, I appreciate you taking a look at them. I know that any investment of time that you, Aaron, or anyone in this community invests into looking at what I'm doing is a gift (genuinely).

My heart sinks anytime I do something dumb. But I can only do my best - which is what I'm doing.

[Jonathan Washburn]

Eric, admittedly I don't know "nothing from nothing" here. I'm building the plane as I'm flying. But that code snippet you posted is a mathlib conversion of my actual code. I wanted to code as much of this foundational layer as possible without using Mathlib, because I want to get as close to core Lean / type theory as possible.

My sense is that when my statements are converted to Mathlib it makes them appear a little more trivial. However, this might just be the nature of trying to build a theory or all reality from a type theory foundation of "nothing cannot observe itself".

These are tied to recognition relations and physical realizability (defined elsewhere in the framework). They're not just exists-statements; they emerge from the meta-principle with properties like unitarity and periodicity.

I'd love thoughts on making them more rigorous/non-trivial in a minimal setting. If this is still "terrible," happy to learn why and improve! :blush:

This is my real code, as found in ledger-foundation/

````lean4

/-- Foundation 1: Discrete Recognition
    Time must be quantized, not continuous -/
def Foundation1_DiscreteRecognition : Prop :=
  ∃ (tick : Nat), tick > 0 ∧
  ∀ (event : Type), PhysicallyRealizable event →
  ∃ (period : Nat), ∀ (t : Nat),
  (t + period) % tick = t % tick

/-- Foundation 2: Dual Balance
    Every recognition creates equal and opposite entries -/
def Foundation2_DualBalance : Prop :=
  ∀ (A : Type) (_ : Recognition A A),
  ∃ (Balance : Type) (debit credit : Balance),
  debit ≠ credit

/-- Foundation 3: Positive Cost
    Recognition requires non-zero energy -/
def Foundation3_PositiveCost : Prop :=
  ∀ (A B : Type) (_ : Recognition A B),
  ∃ (c : Nat), c > 0

/-- Foundation 4: Unitary Evolution
    Information is preserved during recognition -/
def Foundation4_UnitaryEvolution : Prop :=
  ∀ (A : Type) (_ _ : A),
  ∃ (transform : A → A),
  -- Transformation preserves structure
  (∃ (inverse : A → A), ∀ a, inverse (transform a) = a)

/-- Foundation 5: Irreducible Tick
    There exists a minimal time quantum -/
def Foundation5_IrreducibleTick : Prop :=
  ∃ (τ₀ : Nat), τ₀ = 1 ∧
  ∀ (t : Nat), t > 0 → t ≥ τ₀

/-- Foundation 6: Spatial Quantization
    Space is discrete at the fundamental scale -/
def Foundation6_SpatialVoxels : Prop :=
  ∃ (Voxel : Type), PhysicallyRealizable Voxel ∧
  ∀ (Space : Type), PhysicallyRealizable Space →
  ∃ (_ : Space → Voxel), True

/-- Eight-beat pattern structure -/
structure EightBeatPattern where
  -- Eight distinct states in the recognition cycle
  states : Fin 8 → Type
  -- The pattern repeats after 8 steps
  cyclic : ∀ (k : Nat), states (Fin.mk (k % 8) (mod_eight_lt k)) =
                         states (Fin.mk ((k + 8) % 8) (mod_eight_lt (k + 8)))
  -- Each beat has distinct role
  distinct : ∀ i j : Fin 8, i ≠ j → states i ≠ states j

/-- Foundation 7: Eight-beat periodicity emerges from stability -/
def Foundation7_EightBeat : Prop :=
  ∃ (_ : EightBeatPattern), True

/-- Golden ratio structure for self-similarity -/
structure GoldenRatio where
  -- The field containing φ
  carrier : Type
  -- φ satisfies the golden equation
  phi : carrier
  one : carrier
  add : carrier → carrier → carrier
  mul : carrier → carrier → carrier
  -- The defining equation: φ² = φ + 1
  golden_eq : mul phi phi = add phi one

/-- Foundation 8: Self-similarity emerges at φ = (1 + √5)/2 -/
def Foundation8_GoldenRatio : Prop :=
  ∃ (_ : GoldenRatio), True

````

[Aaron Liu]

unknown identifier 'PhysicallyRealizable' :(
It looks like you still need to do some work

[Jonathan Washburn]

@Aaron Liu - If it isn't already super clear - I have no idea what I'm doing lmao. :rolling_on_the_floor_laughing: :sweat_smile: but I'm trying. :man_shrugging:

I have a goal. I can either give up, or do my best to accomplish it. Right now I'm still trying, but trying to get these Lean proofs done, from a cold start, has been brutal.

[Aaron Liu]

this error message is Lean complaining that it doesn't know what PhysicallyRealizable means

[Jonathan Washburn]

Thanks!! working on it now. :)

this reminds me of a story I once heard in church as a kid. There was a boy walking along the beach and there were thousands of sand dollars washed ashore. And the kid was throwing them back into the water, and the old man said - why are you wasting your time with that sand dollar, there are millions of them on the beach - you can't possibly make a difference. Then the kid pick up another sand dollar and threw it into the ocean, and said "it matters to that one".

That's how my code feels. I know there are a million things like PhysicallyRealizable, that I don't know about and make what I'm working on invalid. But each one moves me forward. So thank you.

[Jonathan Washburn]

lol. yes it does feel a lot like throwing rocks at the moon. I'm on day 45 spinning my wheels on it.

[Arthur Paulino]

I empathize with your enthusiasm so I'm going to spend some more time here to provide more food for thought.

In my current understanding about formalization, you need a vision for the scope of your formalization effort, which usually comes with a theorem at the top of your dependency tree (theorems can depend on theorems, axioms, definitions etc).

So you normally start with your types and definitions. This is where you describe the abstract objects you're going to work with. If you vibe code this phase, it generally means one or two of the following:

• You don't know what you're talking about
• You don't know how to translate your thoughts to Lean entities

The former is a dead end. If it's just the latter then learning Lean is pretty much the only way to go otherwise you won't be able to validate what an AI will spit for you.

Once your types and definitions look correct – that is, they faithfully represent what you want to work with – then you state the theorem(s) you want to prove. Here, vibe coding is more welcome, though likely an overkill. Stating theorems is expected to be a smooth experience if you have your types and definitions well set.

Now, proving your theorems is where automation is more than welcome. However, theorem proving is far from easy (very far) and thus automated solutions usually lag behind. At least that's how it's been for the last decades.

---

For example, suppose we're talking about natural numbers. You explain to me what a natural number is and you tell me how to add two of them. I nod and accept your design. Then you tell me "now, if I add $a$ and $b$ I get the same result as if I add $b$ and $a$". I would challenge you. You give me a proof but it's too complicated for my poor intellect. So I propose a protocol: encode the ideas you explained to me in Lean and let me review them... if you're able to convince Lean's kernel of your theorem then I will accept your proof because I trust the Lean kernel.

---

Coming back to your project, that's why people are asking for this sort of framework. They want to see your definitions and ultimately your theorem statements (and vibe coding here will mostly certainly be frown upon).

[Jonathan Washburn]

@Arthur Paulino This is super helpful. Thank you. I started with a traditional journal type paper for the structure of the proof. But I didn't understand or know about - Types & Definitions / mathematical objects (Recognition Science entities, gauge fields, mass gaps, etc.). I'm just now diving in. (Yes, I realize I know less than zero here and this gaff is embarrassing).

[Yan Yablonovskiy 🇺🇦]

Jonathan Washburn said:

Aaron Liu - If it isn't already super clear - I have no idea what I'm doing lmao. :rolling_on_the_floor_laughing: :sweat_smile: but I'm trying. :man_shrugging:

I have a goal. I can either give up, or do my best to accomplish it. Right now I'm still trying, but trying to get these Lean proofs done, from a cold start, has been brutal.

What is the goal in the end ? You already seem entirely convinced of your theory of reality. So is the goal then to actually have others understand it and agree with it?

Or is the goal to have it in Lean? I think the first step is always to have others understand the written math and proofs.

If people can’t understand the written math and proofs there’s no point of Lean.

Since you are convinced , to convince others you’ll need to meet us at our level — rather than say “I will succeed and I am correct “.

Yang-Mills has $1M prize associated with it does it not, you said outside perspectives help etc. There are billions of outside perspectives , the question is what sets yours apart (don’t need to reply to this , point is outside perspective is not a sufficient condition).

[Jonathan Washburn]

@Yan Yablonovskiy The main reason that I want to have it in Lean is that it creates a shorthand for people to know that it's, at the very least, not completely a crackpot theory. It shows some level of structure and formalization - at least enough to stand on it's own and be worthy of someone investing time into it, to explore it's actual merits. (i.e. "have others understand the written math and proofs.")

...that actually may be my secondary or tertiary goal - my primary goal is that I thought that formalizing it in lean would expose any internally inconsistent elements and help me develop the theory further. Another key part is that the theory predicts that reality operates on something coined "Light Native Assembly Language" - basically, like a compile for a computational reality. If that is true, then having the rules of reality codified, becomes important.

"to convince others you’ll need to meet us at our level" - well yes, and more than that. There is no other level, there is only the correct level. So it's 100% my responsibility to get there. I am certainly not asking for special standards. The opposite is true - I must deliver at the highest level of standards.

The issue becomes, do I waste the community's collective time with bogus code. I personally don't think that I'm doing that. I posted one post (this one) about my first Lean project in the "new members" channel. I got some feedback, and I went to work to implement the feedback. And I'm still working on the feedback that I'm getting.

I haven't posted a second proof, or even said that I've been able to incorporate the feedback yet. So I don't think that I'm acting out of turn here. I'm engaging with feedback and criticism - I haven't pushed back on any of it. I've been grateful, and responsive.

Now, I'm committed to figuring it out, but that's a good thing, right?

"There are billions of outside perspectives , the question is what sets yours apart"
Mine is based on a new, deeper understanding of reality. When you have this framework, these harder questions can be answered.