EPR paradox formalization

Stream: PhysLean

[Rein Zustand]

I already had Claude Code with Opus 4.5 to formalize it, and it's done. Currently checking if it compiles, and if it does, I will have to trace the reasoning manually before submitting a PR for it.

[Joseph Tooby-Smith]

With things generated by AI, it’s also important to make sure it fits with the style of the codebase and integrates well into it. We want general APIs where possible with results that can be reused in different areas.

[Rein Zustand]

I indeed had seen a similar remark by you in this Reddit post. I think fleshing out the style further will help both humans and AI in the effort.

[Rein Zustand]

Update on my end: Claude Code + Opus 4.5 had managed to specify spin systems, up to 2-qubit systems specifically. But it struggled with specifying Bell states, with errors after errors, and cutting some corners. I suppose we are not there yet with vibe proofing in the sense of Erdős problem 1026. You could say because that there has been no RLVR for physics formulations yet.

Disclaimer: I don't know how to Lean, still new to me. But I am from Zulip community, where the Lean prover (and Mathlib) community is celebrated.

[Joseph Tooby-Smith]

I think for this we would eventually want to build it on from the API detailed here:
PhysLean#848