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: Nov 21 2024 at 12:39 UTC