Verbal skills are apparently more predictive of programming career success than math scores.

Is Quantum Logic the correct propositional logic? Is Quantum Logic a sufficient logic for all things?

I'd much rather work with machine-checkable proofs; though Lean is not what I've been taught math in either.

Coq-HoTT is written in Coq, not Lean.

A tool that finds the correspondence between proofs as presented and checkable proofs in a reasonable syntax would be helpful, I think.

If I start with "Why is 2+2=4?" [in this finite ring], I'm not sure how to find the relevant Lean code in Mathlib to prove my bias inductively, deductively, or abductively