Comment by data-ottawa

I think it’s a lot like R vs SAS or Python and not any departure from the norm.

Mathematicians are not highly technical users that generally like programming. If you give them a path of importing someone else’s work they’ll do that instead of redoing it in their theorem prover of choice.

See the old mathematician joke:

A mathematician is asked to make tea. They take the kettle from the shelf, fill it with water, put it on the stove, turn on the heat and boil the water, then pour it into a cup.

The next day someone asks the mathematician to make tea again. The kettle is still on the stove from yesterday and there’s some leftover water in it, enough for tea.

The mathematician dumps the kettle out and puts the it away on the shelf. The mathematician says the system is in a known previously solved state and therefore trivially solved.

Now substitute 1500 lines of coq or lean for the kettle. As far as I know the outputs aren’t interchangeable like a vim or eMacs text file.