Aristotle on PhysLean

Stream: PhysLean

[Joseph Tooby-Smith]

I was speaking with @Ronan Lamy yesterday about the use of Aristotle on PhysLean. I'm generally interested to know peoples opinions of it (specifically in regard to PhysLean, to make this specific to this channel), and where we might be able to use it.

I would be interested to know how good it was at solving any of the sorryful results in: https://physlean.com/TODOList

[Anthony Wang]

I tried Aristotle for RigidBody.solidSphere_inertiaTensor but it wasn't able to fill in the sorry.

[Ronan Lamy]

Well, it worked for me. See the raw result from Aristotle here. For future reference, here's what I did:

• Checked out 674aae027ca420dd70eccca7f0a77680a657e003 (the last commit compatible with Mathlib 4.24.0) in a separate worktree.
• Ran lake exe cache get and lake build.
• Submitted PhysLean/ClassicalMechanics/RigidBody/SolidSphere.lean in the aristotle TUI.
• Renamed the resulting SolidSphere_aristotle.lean to SolidSphere.lean (processing took 1-2 hours).
• The result doesn't build due to a syntax error (you can't put a docstring on a section) but the fix is trivial.

@Anthony Wang What did you do exactly? Did you get an error message?

[Ronan Lamy]

Though it's nice to get a proof of a non-trivial result with very little work, I think there's quite a lot of work required to turn it into an acceptable PR for PhysLean:

• The code needs a lot of reformatting to follow our coding conventions, e.g. removing all the semicolons, expanding exact? and non-terminal aesops, etc.
• The struture of the proof is hard to follow, it's probably more complicated than it needs to be.
• Porting it to the current HEAD is nontrivial due to the Space refactoring.

[Anthony Wang]

I tried it around 3 or 4 weeks ago so Aristotle probably has improved since then.

[Anthony Wang]

Aristotle's proof seems shorter than I expected.I've been working intermittently on proving RigidBody.solidSphere_inertiaTensor for the past month by first explicitly defining the homeomorphism for spherical coordinates and using that to solve the integral, which is different from how Aristotle did it.

[Ronan Lamy]

@Anthony Wang AFAICT, it uses symmetry arguments to prove that the off-diagonal elements are 0 and that the diagonal ones are related to ∫ x in Metric.closedBall (0 : Space 3) R, ‖x‖^2. To compute the latter, it uses MeasureTheory.integral_fun_norm_addHaar to change to polar coordinates. Also, TIL that this works:

example (R : ℝ) : ∫ x in 0..R, x ^ 4 = R^5 / 5 := by norm_num

[Anthony Wang]

Oh interesting, I didn't know about MeasureTheory.integral_fun_norm_addHaar! I tried using MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd, which is what the Gauss's law proof uses, but I couldn't get it to work for this proof.

[Joseph Tooby-Smith]

Ronan Lamy said:

Though it's nice to get a proof of a non-trivial result with very little work, I think there's quite a lot of work required to turn it into an acceptable PR for PhysLean:

• The code needs a lot of reformatting to follow our coding conventions, e.g. removing all the semicolons, expanding exact? and non-terminal aesops, etc.
• The struture of the proof is hard to follow, it's probably more complicated than it needs to be.
• Porting it to the current HEAD is nontrivial due to the Space refactoring.

I think we could use this as a good indication of needed/wanted API for the new definition of Space. Maybe worth having a file ".../Space/Integrals.lean" for API related to integrals on Space, or subspaces of Space.

[Joseph Tooby-Smith]

Also, we probably need a better API around Rotations of points on Space.