New to Lean — did I formalize these proofs correctly?

Stream: new members

[Shiva Meucci]

Hi everyone! I'm new to Lean and to this community. I've been working independently on formalizing two results connecting polyhedral geometry, number theory, and group theory. Both compile without "sorry" or custom axioms, but I have no formal training in theorem proving and I'm genuinely unsure whether I've made subtle errors in my definitions or proof structure. I'd really appreciate experienced eyes telling me if I've done this correctly.

The two results:
1. Every prime is a forbidden harmonic. A forbidden harmonic degree of a rotation group G is a frequency ℓ admitting no G-invariant spherical harmonic. I prove that every prime is a forbidden degree of some finite rotation group (constructively, via hyperoctahedral groups B_n). The forbidden sets nest — Forb(T) ⊂ Forb(O) ⊂ Forb(I) — and the icosahedral group sits at the top, capturing all primes up to 29 = |I|/2 − 1. I prove the icosahedron is the unique Coxeter-derived rotation group (in any dimension) achieving maximal Molien saturation, and that the geometric obstruction forces supersingularity for the same ten primes through a triangle group bridge connecting Klein's j-function to the modular form spaces. At p = 37, the icosahedral structure can no longer saturate the modular form space, and the correspondence breaks.

Paper: https://doi.org/10.5281/zenodo.18696119 Lean source: https://github.com/SteamPunkPhysics/Primes-as-Forbidden-Harmonics Lean code DOI: https://doi.org/10.5281/zenodo.18695616

2. The unique forward-closed polyhedral loop. Starting from the tetrahedron, there is exactly one closed forward cycle through regular and semi-regular polyhedra using only rectification, dualization, stellation, continuous deformation, and subset extraction — no operation reversed. The path reaches the rhombic hexecontahedron (60-face saturation of the icosahedral group) and returns to the origin entirely through forward operations. Closure is forced by the identity φ⁸ + φ⁻⁸ = 47, with the fractional parts summing to exactly unity.

Paper: https://doi.org/10.5281/zenodo.18616732 Lean source: https://github.com/SteamPunkPhysics/Polyhedral-Loop-Lean Lean code DOI: https://doi.org/10.5281/zenodo.18616695

Any feedback is welcome — whether it's "your definition doesn't capture what you think it does," "this step is wrong," or just "your Lean style needs work." I'm here to learn. Thanks!

[Martin Dvořák]

I looked at your first project.
Good news: Your project compiles and the main result depends on standard axioms only.
Bad news: Your main result, after unfolding definitions, says:
{2, 3, 5, 7, 11, 13, 17, 19, 23, 29} = {2, 3, 5, 7, 11, 13, 17, 19, 23, 29}
There is literally no mathematical content in your main result.
It begs the question: What's the point?

[Shiva Meucci]

Ack! Yes, thanks.

Where the Real Content Lives (and Why It Doesn't Count)

The project does contain real work:

• Individual proofs that each degree satisfies IsForbiddenDegree (actual semigroup arithmetic)
• The "|Forb(G)| = |G|/4" counting theorem
• The 7+4+4 decomposition, icosahedral uniqueness, etc.

But these are side theorems that don't feed into "main_theorem". The main theorem doesn't depend on the fact that the elements of "forbI" were proven forbidden — it just compares two pre-written lists.

Okay. Yeah, that was dumb.

What Needs to Change

The formalization needs to be restructured so that "forbI" is computed from the predicate, not hardcoded

The fundamental issue: the definitions that should be theorems are being treated as definitions. The supersingular primes are hardcoded as "sspList", the forbidden sets are hardcoded as "forbI". The mathematical content is in why those are the right sets, and that's exactly what's missing from the proof chain.

Thanks so much for your help!!! (Geez this is a mess without another set of eyes. You can twiddle till compile and end up accomplishing nothing)

[Ruben Van de Velde]

Are you using an LLM to write your comments here?

[Shiva Meucci]

I use them to help me edit longer content and write more clearly. Is that a problem? Though honestly, since I've been writing articles for 20 years, there's not much of a difference between my style and an LLM. (people like me are who they got their style from after all)

I hope you don't need me to typo, run-on, avoid punctuation, and poorly capitalize to feel human warmth.
(incidentally, I overuse parenthetical statements and don't use LLMs for short form communication like this)

[Shiva Meucci]

Or did you just want to point out you're better than me both morally and intellectually for not using new tools?

I also can't use a slide rule and I'm sure you can, so I bow to your superiority, humbly beg your forgiveness, and still ask that you continue to provide guidance regardless of my unworthiness. :P

Seriously though, I really do appreciate the help.

[Yan Yablonovskiy 🇺🇦]

Shiva Meucci said:

Ack! Yes, thanks.

Where the Real Content Lives (and Why It Doesn't Count)

The project does contain real work:

• Individual proofs that each degree satisfies IsForbiddenDegree (actual semigroup arithmetic)
• The "|Forb(G)| = |G|/4" counting theorem
• The 7+4+4 decomposition, icosahedral uniqueness, etc.

But these are side theorems that don't feed into "main_theorem". The main theorem doesn't depend on the fact that the elements of "forbI" were proven forbidden — it just compares two pre-written lists.

Okay. Yeah, that was dumb.

What Needs to Change

The formalization needs to be restructured so that "forbI" is computed from the predicate, not hardcoded

The fundamental issue: the definitions that should be theorems are being treated as definitions. The supersingular primes are hardcoded as "sspList", the forbidden sets are hardcoded as "forbI". The mathematical content is in why those are the right sets, and that's exactly what's missing from the proof chain.

Thanks so much for your help!!! (Geez this is a mess without another set of eyes. You can twiddle till compile and end up accomplishing nothing)

To clarify, you are standing by this being written by you and not an LLM?

There is not necessarily a value judgement regarding using LLMs , no one is saying they are better or worse for it. But it is good to clarify and not ideal to obscure it, and in back and forth conversation it is respectful for the others to know that.

I will also add LLM messages that border on being a middleman between the poster and their LLM are heavily discouraged here AFAIK. There is a spectrum on their use.

[Shiva Meucci]

Look. I'm 50. Is the robot emoji thing supposed to intimate I'm not real? I have a hard enough time dealing with all the weird chat tools, having the slightest idea what the right internet etiquette is, no less the sub-community etiquette and ten billion different hieroglyphics kids use to communicate. Can you just cut me some slack?

I literally just found out I have a 70% blockage in my heart and I'd like to not stress over people being mean to me for no reason. Is that asking too much?

And to Yan, no, that's a lot longer and more complex than just a conversation comment. It's an attempt to communicate complex ideas at the edge and beyond my personal abilities.

Can I not be at the business end of a witch hunt within three posts in a new place?

Why is my blood pressure through the roof right now just for the sin of daring to ask for help? How much do you need to shame me to feel satisfied? What is the exact amount of pain you need to inflict to let up and move forward?

[Shiva Meucci]

PS: Even the quoted section that was LLM edited was also human edited, transformed, and added to. ...just so you know I never just blindly interpose an LLM between me and other people. (but I am a prolific writer and writing things like "ur" is viscerally revolting to me)

[Shiva Meucci]

...oh, and thanks for removing the robot emoji from my third post. Sticking a robot on every post I was making felt particularly mocking.

[Kyle Miller]

I can't speak for others, but from my perspective this community has had a lot of AI-generated/assisted content recently, and it can often feel like engaging with these posts has an energy imbalance — I like teaching people, but it doesn't feel great if people take what I say, copy it into an LLM, then reply with what it says, even if it's edited. It becomes impossible to tell if the person in the loop is learning anything if it's all being filtered through an LLM.

I'm not saying this is what you're doing @Shiva Meucci — I'm just trying to give context that's hard to see as an individual among a rising sea of other AI users — please stick around, follow what's going on here, learn what you can from the community! Please don't take it personally if people here need some "proof of work" so to speak, that the time and attention is aiding a real person's learning efforts.

How I've seen people use :robot: is "this looks AI generated", not "this is user isn't human" (though we've seen a number of almost-surely non-human users!). I'll say this: I can recognize the ChatGPT style from my own overuse of it, and there's something unfocused and nonspecific about how it speaks about technical things that has been bugging me more and more. If I want to be bugged, I think I'd rather go and drink from the unfiltered source itself :-)

[Shiva Meucci]

Thanks so much for the explanation @Kyle Miller. I can understand the issue of spam. (We all do)

The question I have is this, though: As I said. I'm an older man. I learned C way back and a few other ancillary languages. I've had to put up with some python now that it's ubiquotous. I've learned a million little tools for all the various one-man-show things I have to do. I learned the whole field of neuroscience because my wife was doing her bachelors and I went to all the classes. I'm now in a production mode.

Does it make sense for your community to reject my attempt to use this incredible contribution to the world called "lean" because I simply cannot add learning another language to my plate and ever accomplish my goals which are tangential to (but aligned with) the goals of the community?

Is it valueless for someone to help me build out a proof into the lean language instead of publishing it without lean? If I am possibly able to augment a History-of-Physics program with a mathematical proof in a way that could change our perspective on historical interpretations of physics - thus opening cracks through which new light can shine on the weird disconnects in today's program - but then I "merely" use lean to show that it works while never learning lean and never intending to learn it, have I abused the trust or work of those in the community supporting and even creating this fabulous system for verification?

(and is that a long enough sentence to show I didn't use LLM editing? lol)

I think the answer is a resounding no.

So, yeah, I must admit I don't intend to learn the language well enough to be competent. I want to use it to do something else I'm doing which may in fact be very valuable and important - and it is my earnest belief that is so. Is that somehow off-putting?

I am using other people's time with respect, appreciation, and only putting it towards something I value greatly. I put my own extreme effort into that same project but from an entirely different direction.

I think the respect and value of the time of others and consideration of community effort is what is key, isn't it?

I am never punching a few keys and walking away or putting in trivial effort while asking others to put in real effort. If I ask for the help of another, I will have always put in at least ten times more effort than they have beforehand because I understand and respect the value of another person's effort. I'm just not a taker like that.

I know that's rarely the case and you can only use statistics and heuristics to decide how to use your time, but perhaps you can go just a hair easier on people using AI if they also seem to be putting in effort and respecting yours?

...and incidentally, looking at your icon, I hope you love Kelvin as much as I do and did you know that J.J. Thomson produced the first workable physical explanation of atomic valence based on knot theory?? So cool.

[Kyle Miller]

Shiva Meucci said:

I will have always put in at least ten times more effort than they have beforehand because I understand and respect the value of another person's effort

I think this community tends to recognize genuine effort and responds in kind. People are also really busy, and it can take awhile for the right people to pop in with help or advice.

You should expect needing to get to a certain level of understanding and familiarity with Lean to make progress. The bare minimum is being able to read the definitions and theorem statements and to be able to evaluate for yourself whether these are accurate. This is something people will be happy to help with, but rather than "here's a dozen files, please evaluate them", I think tends to be more effective when people identify a gap in their own understanding and post here a self-contained 5-15 line snippet (a "#mwe") that illustrates the issue.

What I see in AI-written Lean projects with novice Lean users is that the AI has convinced the user that the project does what it says it does, partly by including many comments giving the illusion that something has been done, but the theorems are largely simple arithmetic with no real content. I read through a number of files, including this one for example, and the comments claim there are these proofs about finite reflection groups, but the Lean itself has no bearing on finite reflection groups — it's all a bit of natural number arithmetic. I'm sure this was all a reasonable amount of effort on your part, but, please don't take this the wrong way, I'm sorry to say that it appears that the AI's fooled you :-( I looked through 10-15 files between the two projects, looking for anything, but there's no content, except for two things: (1) a couple identities involving the golden ratio, and (2) an inefficient version of Euclid's algorithm. This might not be the feedback you were hoping for.

I don't believe this community rejects casual Lean users at all. I think it's likely that if you start this project from the beginning and develop it step-by-step in the open, you'll get useful feedback and help.

Shiva Meucci said:

I hope you love Kelvin as much as I do and did you know that J.J. Thomson produced the first workable physical explanation of atomic valence based on knot theory??

I've enjoyed the stories of the origin of knot theory via the vortex model of the atom. Gauss too was an early investigator; I understand he studied the magnetic fields of knotted loops of current.

[Martin Dvořák]

As @Kyle Miller just said, it seems to be the case that the AI has fooled you. And it would be better to find out that you cannot trust the AI on a small example, before you share two large projects where there is suddenly "too much to unpack".

[Arthur Paulino]

My honest tip for beginners who want to use AI with Lean is to, at the very least, learn enough to write the definitions and the theorem statements by hand, leaving theorem proofs as sorrys. This way, one is forced to know what the code is talking about.

Then ask for help from AI to replace sorrys by actual proofs. Here, you might find out that AI will sometimes struggle to get things correct. It often spits proofs that aren't accepted by Lean.

Important: asking for feedback on your handwritten definitions and theorem statements is absolutely fine. Sometimes, even when you encode the right idea (mathematically speaking), it might not be the best design choice for a theorem prover. And the community has members with enough experience to help you there.

[suhr]

Arthur Paulino said:

My honest tip for beginners who want to use AI with Lean is to, at the very least, learn enough to write the definitions and the theorem statements by hand, leaving theorem proofs as sorrys. This way, one is forced to know what the code is talking about.

There's one problem with this: proving is exactly how you understand and tweak definitions.

My advice is a bit different and more general: don't use AI to do something you don't see how to do yourself.

[Shiva Meucci]

Thanks for the advice!

This is something where I took on a bit more than I could handle in an already far overtaxed workload and it might be a case for paying more attention to the Icarus story. If I could bother any of you for just one more cursory eval, it could really help me gauge the distance I can take this and the value (or acute lack thereof) of the previous workflow and how far I am from goal. I might have to face that it may just demand more than what I can take on at the moment. I'd hate that, but forward momentum often requires letting go of some idealism.

The 2nd proof on this list was much simpler. (As a paper) It was the first. Is it just as bad? It seems you can kinda tell at a glance because of your experience. I presented them in reverse order because the second was the one I had the least confidence in. If the first is just as bad off then I need to take a very big step back.

Lean has gotten a reputation for "if you make it compile, it's worthwhile." ...and that's obviously just not even remotely true. Seems like maybe it needs a tautology checker like checking for sorryAx?

[Snir Broshi]

Lean has such things, see https://leanprover-community.github.io/did_you_prove_it.html and https://github.com/leanprover/comparator (but not for tautology AFAIK)

[Snir Broshi]

Could you point at where you want help at? Which theorem?

[Shiva Meucci]

Since I (too easily) believed everything was working, this whole proof chain is now suspect. When you think everything is okay, it's hard to know where to start to look for what's wrong. This should be mostly (fairly) straight forward geometry in most of the files. I'm not re-proving Klien etc.

I guess the place that is most suspect might be the top-level Synthesis? If the steps are defined with named endpoints and closure is proved by "rfl/simp", that could collapse to “the path we wrote down is closed,” not “the constraints force this path/terminal point,” right?

...but in general, if the whole damn thing is a mess instead of specific difficult points, then it's probably best to just give up the whole endeavor.

https://github.com/SteamPunkPhysics/Polyhedral-Loop-Lean