feat: create physlean announcement#131
feat: create physlean announcement#131herostrat wants to merge 2 commits intoleanprover-community:masterfrom
Conversation
|
Hey @herostrat, many thanks for doing this! I think there are some inaccuracies in the post, but more importantly, we currently undergoing a merger with the which probably changes things a lot |
|
Oh, I didn't know this! I added my proposal. If there is interest from your side: feel free to change or suggest changes for me to implement. Btw: I love it that there is increasing traction on the physics side. Imo that's because of your dedication! |
Vierkantor
left a comment
Vierkantor
left a comment
There was a problem hiding this comment.
Please let me know when the blogpost is ready and I will check it in detail!
| - **Quantum information theory**: formalizations of quantum channels, entanglement, and related concepts from the QuantumInfo project. | ||
| - **Statistical mechanics and condensed matter**: early formalizations of foundational concepts. | ||
|
|
||
| To give a flavor of what formalized physics looks like in Lean, here is a simplified example. The commutation relation between creation and annihilation operators for the quantum harmonic oscillator, $[a, a^\dagger] = 1$, can be stated and proved as a theorem in Physlib, building on Mathlib's algebra and analysis libraries. |
There was a problem hiding this comment.
Can you give a link to the statement here? Or perhaps even an editable snippet, a la https://live.lean-lang.org/?
| @@ -0,0 +1,86 @@ | |||
| --- | |||
| author: 'Joseph Tooby-Smith' | |||
There was a problem hiding this comment.
Author may need to be the author of the blog post.
| type: text | ||
| --- | ||
|
|
||
| Joseph Tooby-Smith introduces [Physlib](https://physlib.io)<!-- TODO: update URL -->, a community project to formalize physics in Lean 4. |
There was a problem hiding this comment.
Maybe
We introduce [Physlib](...)...
| - **Classical mechanics and electromagnetism**: including formalized versions of the Lorentz group and its properties. | ||
| - **Quantum mechanics**: the quantum harmonic oscillator, creation and annihilation operators, and their algebraic relations. | ||
| - **Quantum field theory**: Wick's theorem for both bosonic and fermionic fields, a key result used throughout perturbative QFT. | ||
| - **Particle physics**: the structure of the Standard Model, including its gauge group $SU(3) \times SU(2) \times U(1)$, the Higgs mechanism, and anomaly cancellation conditions. |
There was a problem hiding this comment.
Not quite the structure of the SM
|
|
||
| The combined library, now hosted under the leanprover-community organization as Physlib, covers a broad range of physics. The library currently includes formalized material spanning: | ||
|
|
||
| - **Classical mechanics and electromagnetism**: including formalized versions of the Lorentz group and its properties. |
There was a problem hiding this comment.
Lorentz group should probably be under special relativity.
|
|
||
| Beyond building a library, Physlib has several longer-term aspirations: | ||
|
|
||
| - **Making physics results easier to locate and reference.** A formalized library is also a searchable, cross-referenced database. Instead of hunting through textbooks for the right form of a result, you could query Physlib directly. We already have a search tool at [loogle.physlean.com](https://loogle.physlean.com)<!-- TODO: update URL --> for this purpose. |
There was a problem hiding this comment.
loogle doesn't work anymore for PhysLean :(. Couldn't justify the server costs
|
|
||
| To help you get started, we provide: | ||
|
|
||
| - A **live editor** at [live.physlean.com](https://live.physlean.com)<!-- TODO: update URL --> where you can experiment with Physlib in your browser. |
| To help you get started, we provide: | ||
|
|
||
| - A **live editor** at [live.physlean.com](https://live.physlean.com)<!-- TODO: update URL --> where you can experiment with Physlib in your browser. | ||
| - A **search tool** at [loogle.physlean.com](https://loogle.physlean.com)<!-- TODO: update URL --> for finding definitions and theorems. |
|
@herostrat, 🏓 |
4 participants
Hey @jstoobysmith
it took a long time but I as I was looking through my open issue I found the blog post one from long ago.
I decided to write something up (together with claudes help) and ask what you think about it.
LMK what you think :)
Fixes: leanprover-community/physlib#158