hol-light 20231021-1 (armhf binary) in ubuntu noble

 HOL Light is an interactive theorem prover for Higher-Order Logic
 with a very simple logical core running in an OCaml toplevel. HOL
 Light is famous for the verification of floating-point
 arithmetic as well as for the Flyspeck project, which aimed at the
 formalization of Tom Hales' proof of the Kepler conjecture.