News for hackers. Stuff that matters.
Re:Computation as a Universal and Fundamental Concept by jesuslop on Friday July 10, 2026 @08:59PM (#48867410)
I think Gödel undecidable sentence is always relative to a formal system (the title of the paper spoke about systems in the expressive power rank of Russell's Principia, of which he gives one particular example assuming it shows how his methods apply to the whole family of systems), but now Hilbert problem #6 still stands for the lack of a comprehensive axiomatization of Physics, as its modern heir the mass-gap millennium problem, that still also lingers, so we don't have a controllable notion of naked/absolute undecidability for physical phenomena or for arbitrary assertions unbound by explicit logic rules in general.
Re:Computation as a Universal and Fundamental Concept by peter_m1 on Saturday July 11, 2026 @09:02AM (#48871696)
Also, correct me if I'm wrong, the mass gap problem involves quantum physics, not classical, so the underlying math/logic is different.
Re:Computation as a Universal and Fundamental Concept by jesuslop on Saturday July 11, 2026 @02:21PM (#48874354)
mmh I'd don't say that much, I think the logic and math foundations is common in both classic and quantum theories, only content changing, so you would say "import mathlib" from both classic-phys.lean and quant-phys.lean if writing Lean proof assistant code (I am guessing the "import" command). Concepts from linear algebra as eigendecomposition, to say something, will be used in both applications.