In my humble opinion, a possible research project involving both machine learning and Isabelle/HOL may be as follows:

(i) to develop mathematical structures which are involved in modelling learning processes, e.g., Hilbert spaces, measure theory and probability, the Fokker–Planck equation.

(ii) to formalise well-known theorems in this field and maybe new theorems.

In a rather indirect way, anyone who is developing a mathematical structure, which can be used in modelling learning processes, is contributing to part (i) of this hypothetical research project. Part (ii) is more specific.

Last updated: Dec 07 2023 at 16:21 UTC