Awarded NSF AIMing grant (lead PI) on neuro-symbolic approaches to mechanized mathematical reasoning.