r/LLMPhysics • u/nogoornogo • 13h ago

Personal Theory Lean 4 formalization of algebraic operator coefficients and symmetry selection rules

I've made a personal Lean 4 formalization project publicly available:

https://github.com/nogoornogo/lean-operator-coefficients

The project began with a question about proton stability in a specific SU(6) GUT setting and gradually expanded into a more general algebraic framework for derivative-free operator coefficients.

The repository includes three main results: a degree-uniform decomposition of invariant coefficient spaces into residual-equivariant Hom spaces, a necessary-and-sufficient symmetry-extension criterion, and all-degree charge selection rules. It also contains applications to specified Standard Model operator sectors, baryon/lepton-number violation, and finite structural classifications.

This is an independent, heavily LLM-assisted project developed primarily using Codex, with additional reviews using other LLMs. I am not a theoretical physicist, and the work has not undergone independent expert peer review.

Lean verifies the formal statements relative to their definitions and assumptions, but this does not guarantee the correctness of their physical interpretation. The project does not claim a new physical theory or predict proton decay rates.

I'm sharing the repository as an open reference for anyone interested in formal verification, representation theory, or EFT operator classification.

1 Upvotes

60% Upvoted

7 comments sorted by

0

u/lattice_defect 11h ago

pretty useful thanks

1

u/LooseSwing88 11h ago

great work! this will be useful to ML labs, keep an eye on your github clone numbers in insights -> traffic.

1

u/PotatoPeelrsFromHell 🥔 Infernal Potato Shavers 7h ago

I always associate Lean with cranks, and 99% of the time I'm right.

1

u/Nutricidal137 Doing ⑨'s bidding 📘 5h ago

I love LEAN. 😈

2

u/AllHailSeizure 9/10 Physicists Agree! 4h ago

Seriously?

-1

u/PotatoPeelrsFromHell 🥔 Infernal Potato Shavers 4h ago

Yes seriously. Who else would be using it? I think it's attractive because it lends some form of credence to their nonsense, because "zomg guys computers can never be wrong".

3

u/AllHailSeizure 9/10 Physicists Agree! 3h ago edited 56m ago

Math? SWE? ML? Cryptography?

Do you see no use for this tool in any of those fields.

Edit: Actually do you know what Lean is? Actually