Skip to content
Date: 28th January 2022
Time: 14:00 - 16:00
Location: Hybrid Meeting (G.03)

Title: Mechanising Newtonian Mechanics in Isabelle
Speaker: Lars Werne

The Isabelle Theorem Prover is an interactive framework for developing formal mathematical theories that checks proofs for validity using the rules of Higher Order Logic. In my talk, I will present the state of my project on the mechanisation of Newtonian mechanics using this framework.

In my work thus far, I have focused on the interplay of forces acting on point particles and their position, velocity, and acceleration, based on Newton’s fundamental laws of motion and previous results on abstract analysis from the Isabelle proof library. In the coming months, some of main aims will be to generalise my current implementation so that “space” is treated as an arbitrary real vector space, and expand on my results on central, conservative forces and their properties