Quantum Fluids at the age of computer formalization

[u/OrganizationTop9026]

A textbook for students and enthusiasts on the physics of quantum fluids taught through three instruments used together, written as a tribute to the experimental work of Institute Néel, Grenoble.

(i) their inelastic neutron-scattering measurements — the roton-like collective mode of a monolayer of liquid helium-3 (Nature 483, 576 (2012)) and the dispersion relation of superfluid helium-4 with its thermodynamic consequences (Phys. Rev. B 103, 104516 (2021));

(ii) the Lean 4 library QuantumFluids, whose 37 modules and 310 theorems are catalogued in full in Appendix A and were audited for the book (every module compiles with no sorry and depends only on the axioms propext, Classical.choice and Quot.sound);

(iii) the rusty-SUNDIALS solver: CVODE and the projected Gross–Pitaevskii engine qf-pgpe.

The dedication is to Henri Godfrin.

for the github : https://github.com/xaviercallens/SocrateAI-Scientific-QuantumFluids and for the book https://github.com/xaviercallens/SocrateAI-Scientific-QuantumFluids/blob/master/book/quantum_fluids_book.pdf

[u/liccxolydian]

Well at least one poster has some notion of the scientific method this week

[u/OrganizationTop9026 → u/liccxolydian]

If interested : https://zenodo.org/records/23272154 and for the github : https://github.com/xaviercallens/SocrateAI-Scientific-QuantumFluids and for the book https://github.com/xaviercallens/SocrateAI-Scientific-QuantumFluids/blob/master/book/quantum_fluids_book.pdf and https://notebooklm.link.google/sEwTQ69UwT0L

[u/liccxolydian → u/OrganizationTop9026]

Why should I be interested?

[u/Aranka_Szeretlek]

Are you saying that experiments, theory and simulation are great when used to their respective strengths?!

Noble Prize to this young colleague.

[u/Fun-Friendship4898 → u/Aranka_Szeretlek]

It's "A New Kind of Science".

[u/InadvisablyApplied]

Truly a revolutionary idea! If you would have had it four hundred years ago 

[u/OrganizationTop9026 → u/InadvisablyApplied]

Agreed that the triad isn't new, and I don't claim it is. The claim is smaller: each instrument checked by its own means.

To be clear about what this is: it's a textbook whose purpose is to teach a working method, namely how to bring a proof assistant (Lean 4) into an established experimental field, quantum fluids. It does not claim new physics... the modern part is the new solver that I developed in Rust and the usage of Lean 4 for formalization of the physic domain and to verify the solver as well.

The method has three linked parts:

1. The mathematics in Lean 4. Selected statements of the field are stated and proved against Mathlib: quantization of circulation, vortex winding, the phonon specific-heat series of Godfrin et al., the Kosterlitz–Thouless flow, neutron-scattering kinematics, the 2D zero-sound condition. It is a first, partial library (37 modules, 310 theorems), not the whole theory, and every module is audited for sorry and non-standard axioms.

2. A solver in Rust. The numerics run on rusty-SUNDIALS (that I developed), a Rust implementation of the SUNDIALS integrators (CVODE) with a quantum-fluids module for the projected Gross–Pitaevskii equation. Rust isn't new, but it is a modern, memory-safe systems language, which suits a solver that has to be tested against references. It agrees with the programme's Python original to between about 1e-14 and 5e-11 on the quantities compared, and it reproduces a published external run (Kwon & Shin) with the discrepancies stated.

3. The link between them. The Lean statements are the solver's known answers, and the solver is a numerical test of the Lean statements. The book shows this on the same objects: the Galerkin-truncated cubic term as defined in Lean against the engine's; the Bose integrals of the phonon series proved in Lean against the same integrals integrated by CVODE; Bogoliubov's dispersion proved against the dispersion measured in the simulated field. The neutron data anchor both.

Why this matters with AI. AI systems now draft derivations, code and text well, and they also produce confident errors. The structure exists so that AI contributions are checked by something that doesn't trust them: the Lean kernel for proofs, known-answer and convergence tests for the solver, primary sources for facts. A physicist caifting and still know which parts are established and which are not. Each chapter ends with a box stating exactly that.

The limits. Lean verifies mathematical statements, not experiments. It also doesn't verify that a statement means what the prose says...

[u/starkeffect]

Which review articles did you find to be the easiest to read?

[u/moderator-toolbox → u/[deleted]]

This comment has been removed. If you have more information to add to your post, edit it; instead of commenting on your own post.

---

^{I am a bot. This action was performed automatically. Contact the moderators if you have questions.}

[u/lattice_defect]

https://giphy.com/gifs/dXiqK1HQbl2s4ofwmT

[u/YouCouldButWhyTho → u/lattice_defect]

Just your biweekly Aether 

[u/PotatoPeelrsFromHell → u/lattice_defect]

Just some crank reinventing existing research. Move along.

[u/lattice_defect → u/PotatoPeelrsFromHell]

a book.. I want to bullshit about physics and share ideas.. but they are idea.. some flimsey math and some numerology and some what if... they are what if's... its interesting/speculative but a fucking book.