4 ms·
Also, correct me if I'm wrong, the mass gap problem involves quantum physics, not classical, so the underlying math/logic is different.
by peter_m1 3mo ago
Also, correct me if I'm wrong, the mass gap problem involves quantum physics, not classical, so the underlying math/logic is different.
- jesuslop 3mo agommh 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.