CIRCLE WITH A DOT

@mc I definitely agree with this, and I have a bunch of thoughts about fixing it. Some programmatic remarks:

- Interactive theorem proving and text-based representations are already uneasy bedfellows. Let's embrace the "interactive" part and move to true structure editing where proof data is stored as abstract syntax trees and the language provides an open protocol for interfacing with such ASTs, on top of which one can implement whatever UI one pleases. Text-based editing becomes just one such "view" of the underlying proof data.
- A lot of "ordinary" math comes down to: draw a structured graph (in *both* senses of the word "graph") of some sort, and make some conclusion based on its structure. By now there's plenty of existing work on compiling things like commutative diagrams/string diagrams/etc. to syntax trees, etc., and we can and *should* make use of this work to provide more convenient interfaces to ITPs, via protocols as above.
- Interactive theorem proving deserves interactive documentation. We should have an analogue of Jupyter/Mathematica Notebooks for ITPs where different editor UIs can be mixed and matched, data can be displayed in a variety of formats, etc.

@JacquesC2 @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject

Having spent several years in the trenches of formalized mathematics by now, I'm actually more sympathetic @johncarlosbaez 's line of thinking than I used to be, but I think there's nothing about formalized mathematics *per se* that forces this to be the case.

The way I've come to use proof assistants/etc. over the years actually, counterintuitively, ends up making math more "empirical," in a way. My informal proofs and ideas become "hypotheses" I can "test" by attempting to find a formalism and suitable abstractions that make them checkable by a computer. And like any good scientific experiment, this quickly becomes an iterative process—take some informal ideas, attempt to formalize them, get some data back about what ends up being difficult, refine the ideas, repeat until a satisfactory equilibrium is found. And this process itself can lead to a lot of "a ha" moments and "radical" new ideas, itself.

As already noted, however, this process carries the risk of railroading one's thoughts into those ways of thinking that are more easily formalized in a particular system. But imo this is a failure of that particular system to be sufficiently syntactically/semantically flexible, and not of formalism/interactive theorem proving in general.

The future I hope for, and which I am actively building toward, is one in which we have general systems for defining, simulating, and verifiably translating between different logical/formal systems, so that if someone has a new mathematical idea they want to try out it's easy to get up and running with a system for testing it and relating it to other frameworks.

@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject