[nmca]

Interactive theorem proving is an active area of research, but it's quite hard to do well, and the main area of focus is on theory atm, as opposed to UX