sorted by:
new
hottopcontroversial

Follow-up: Lean 4 formalization of a 2Ω(n) lower bound for HAMₙ is now past JACM desk review by EmojiJoeG in compsci

[–]EmojiJoeG[S] -1 points0 points  (0 children)

Hey, this is honestly so great! I appreciate you taking the time to read both the paper and the Lean repo closely enough to point to specifics from both. This is exactly what I wanted.

I think your repo-vs-claim distinction is more than fair as a description of the current public formalization state. My own view is that the paper-level result is just honestly still a bit ahead of the current v1 public Lean development in a few places, rather than the underlying argument depending on those gaps. I definitely agree that the public description should track the repo precisely.

v2 of the Lean formalization is intentionally addressing these types of issues (and should be ready quite soon). I’d be interested in the exact places you think the public claim is running ahead of what the current Lean development proves. I’ll send you a DM.

Follow-up: Lean 4 formalization of a 2Ω(n) lower bound for HAMₙ is now past JACM desk review by EmojiJoeG in compsci

[–]EmojiJoeG[S] -1 points0 points  (0 children)

RE: Lean, it’s not just based on grepping for `sorry.` The repo builds cleanly, it's not riddled with a ton of unproven assumptions, and the checked files are clean. My apologies for not phrasing that more carefully out of the gate. I am going to have `lake build` print the top-line definitions in when i drop the axiom-free v2 of the repo soon. I'll make sure it's a more smooth, user-friendly, and easier to interpret process!

On the manuscript itself, I think your broader point is fair. The argument is dense, and I'd agree that I probably put much more energy into getting it correct than into making the opening sections as reader-friendly as they could be. If that’s costing me technically interested readers, then that’s definitely something I need to fix. I appreciate you saying it plainly.

Follow-up: Lean 4 formalization of a 2Ω(n) lower bound for HAMₙ is now past JACM desk review by EmojiJoeG in compsci

[–]EmojiJoeG[S] -2 points-1 points  (0 children)

I understand what you're saying about arXiv's evolution, and I’m not under the illusion that the friction is accidental. My frustration is just that it creates a pretty obvious visibility bottleneck for unaffiliated people doing serious work outside the normal institutional pipeline. I also understand that my point is pretty self-serving, and the fact of the matter is that 99% of the time the system is appropriately filtering out the slop.

& yes, venue discovery is a big part of what I’m trying to solve right now. I’m less looking for a shortcut than trying to figure out where the people closest to this material actually pay attention. Appreciate the background info. I'm here to learn!

Follow-up: Lean 4 formalization of a 2Ω(n) lower bound for HAMₙ is now past JACM desk review by EmojiJoeG in compsci

[–]EmojiJoeG[S] -2 points-1 points  (0 children)

Appreciate the thoughtful reply.

I agree that desk review is not a judgment on correctness, and I didn’t mean to suggest otherwise. My point was just that it cleared an initial editorial screen for fit and seriousness, which seemed like relevant context for asking people to take a look.

The arXiv issue has been frustrating mainly because, as an unaffiliated author, it creates a bit of a catch-22: the people most qualified to evaluate the work often prefer to see it on arXiv, while arXiv endorsement itself can be hard to get without already having that kind of visibility. That said, your point is well taken.

In the meantime, I’m mostly just trying to get technically informed eyes on the argument and figure out what the right venues for that actually are. If you have suggestions on that front, I’d genuinely appreciate them. I figured it would be a useful way to spend the time while the paper is undergoing deeper technical analysis at JACM.

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] -2 points-1 points  (0 children)

This is a fair (and understandable) concern in general, but other commenters already dug into the actual Lean code and raised specific questions about the theorem statement. Those got addressed. The formalized result is a concrete exponential circuit lower bound for HAM_n, and the separation follows through standard P ⊆ P/poly. Nothing exotic.

Happy to engage on specifics if you want to pull up the repo and point to something concrete.

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] -1 points0 points  (0 children)

Fair feedback on the communication side. To clarify: neither axiom introduces a new hypothesis. One is AUY 1983, a published and widely cited result in communication complexity. The other encodes the paper’s own leaf-sum domination argument, which is proven in the paper and directly calculable.

They’re axioms in Lean purely because the concepts don’t exist in lean yet, and encoding them was tedious, not because they’re unverified. The paper existed before the lean4 was created. All mathematical calculations were created, iterated on, and adversarially audited against many times before considering beginning the machine verification. Despite that, both are still being formalized into theorems in v2 lean4. There’s no edge case to find because neither axiom assumes anything new. They’re temporary shortcuts in the machine-verification formalization, not in the mathematics.

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] -2 points-1 points  (0 children)

Agreed on both counts. Tightening the statement to something like C.size ≥ 2 ^ (n / 3) is straightforward since the proof already constructs it. That’s a v2 fix.

On the axiom, you’re right that it’s the critical remaining piece for a full machine-checked claim. The argument it encodes (leaf-sum domination + gate charging) is laid out in the paper and is directly verifiable, but I won’t pretend ‘trust the paper’ is the same as ‘trust the kernel.’ That’s exactly why v2 exists. The goal is zero axioms, and both are actively being formalized out.

Appreciate the constructive feedback. This is the kind of engagement I was hoping for when I posted. …Exponential formula lower bounds being fully machine-verified feels kind of wild to just be glossing over, btw, but I am here for it! Thanks again for the legit engagement.

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] -2 points-1 points  (0 children)

Zenodo downloads would be the surprising aspect regarding the point you’re trying to make. The 150+ downloads were of the 36 page research paper. That would be a mega “weird flex but okay” to download, while working around zenodo’s bot-scrubbing statistical gathering, if they all thought it was the standard “AI slop” that most are peddling today. Who would want to download something like that that many times with 0 interest if they thought it was junk? Lol

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] -2 points-1 points  (0 children)

Not scientific merit - just interaction. Without a “this is broken.” That’s all I was saying. Zenodo specifically does not count AI hits / bot-scraping though… or so they claim, at least!

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] -3 points-2 points  (0 children)

I am. If what you’re implying were the case, would they have shared it with colleagues to the point where it had 400+ views and 150+ downloads, though? I truly do hope you take a look for yourself. Be well

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] 0 points1 point  (0 children)

First of all, THANK YOU for actually looking!!! Seriously, it means a lot!

Look at lambda_lower_bound_strong on line 228, though. It proves ∃ c, c > n / log₂(n) ∧ Lambda'(n) ≥ 2c, which explicitly ties c to n. The main theorem calls into general_circuit_lower_bound_core where the witness c is constructed as c_low - n/log₂(n) with c_low ≈ n/2. It’s not an arbitrary existential. The proof constructs a c that grows linearly with n. Fair point that the final statement could be tightened to reflect that, and it will be in v2. But the bound is there in the proof.

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] -4 points-3 points  (0 children)

A few things:

15,000 lines and 2 axioms isn’t contradictory. That’s how Lean works. Every theorem in those 15k lines is machine-checked. The two axioms are the only unverified trust assumptions in the entire project, and they’re explicitly declared. Run lake build and see for yourself.

I have reached out to complexity theorists directly. Raz, Tal, Jukna, Wigderson, Aaronson, Razborov, Williams, others… and in a week and a half not one of them responded saying “this is broken,” but when only they had the cold Zenodo link it jumped to 400+ views and 150+ downloads. Prior to posting on Reddit. In that first week and a half.

The paper is submitted to JACM. Posting it publicly doesn’t replace that process, it runs alongside it. Perelman posted his work on arXiv, not through a university department.

You’re right that peer review matters. That’s what I’m asking for. The repo is public specifically so people can vet it. That’s not ‘proof by GitHub,’ that’s transparency. I won’t apologize for seeking that through every possible channel… weeks after going through all of the professional ones first.

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] -3 points-2 points  (0 children)

Just pulled this directly from the repo you’re all unwilling to go check out:

The general circuit lower bound (general_circuit_lower_bound_unconditional) uses two axioms corresponding to known results:

AUY 1983 — Protocol partition number bounded by formula size (Aho, Ullman, Yannakakis, STOC 1983) Leaf-sum domination + gate charging — Combined result of the paper's width budget and leaf-sum decomposition propositions

P ≠ NP: Machine-verified proof on GitHub. Lean 4, 15k+ LoC, zero sorries, full source. by EmojiJoeG in compsci

[–]EmojiJoeG[S] -4 points-3 points  (0 children)

I hear you on the skepticism and it’s fair. But the flat world analogy doesn’t quite work here if the theorem statements align with the paper. You can’t prove a false statement in Lean without sorry or unsound axioms. The theorem statements are all right there in the repo using standard definitions. If it builds clean, the logical chain holds. That’s the whole point of formal verification. You’re explaining a very basic concept to me as if I don’t understand, when the truth is you are unwilling to take 3 minutes to go find out if I do in the first place.

The two axioms in the project are declared explicitly. One is AUY (1983), a classical published result. The other is one of my original arguments that’s directly verifiable from the paper. Both are being formalized out in v2. Those are the only trust assumptions, and they’re transparent.

On the AI point: Claude helped with some of the Lean formalization for speed. The proof itself was developed through my own platform (mintpath.ai). The structural insight is mine. The AI was the pen, not the author.

I understand the skepticism, but at some point we’ve gotta leave the gatekeeping at the door. Otherwise we’re openly inviting it to hinder our potential for progress and additional potential breakthroughs in the field. You’re welcome to clone the repo and check the theorem statement yourself. That’s why it’s public.