My research currently focuses on developing techniques, often based in computational neuroscience, for mathematical reasoning. I occasionally write about my ongoing projects on this blog:

• Dec '20 : Language learning and program synthesis.

• Dec '19 : Automating proofs of lattice inequalities in Coq using duality.

• Oct '19 : Guaranteeing proof termination: Dealing with infinite proof search.

• Sept '19 : Getting started with proving math theorems through reinforcement learning.