# “Formal Math” - Do you allow sites that don't follow the usual Stack Exchange protocols?

Following discussion with trusted colleagues I am thinking about setting up a site for working on formalized mathematics. To quote John Harrison:

It is generally accepted that in principle it’s possible to formalize completely almost all of present-day mathematics. The practicability of actually doing so is widely doubted, as is the value of the result. But in the computer age we believe that such formalization is possible and desirable. [source]

It occurred to me that the Stack Exchange format could work well to support the formalization process, but the protocols would have to be abused somewhat. Specifically:

1. Instead of a usual "question", each post would be a topic to formalize (e.g., "Hilbert space", "Fermat's Last Theorem").

2. Each "answer" would be a component of the formalization -- a lemma or definition.

The notion of an "accepted" answer would still be meaningful, since this would be the answer that actually formalises the concept under discussion. It would in general build on the other answers.

Other than that, one answer would not be noticably "better" than another answer to a given question -- though they could still be given upvotes to show appreciation or interest. As a whole, each page would be something like the big-list questions which appear on the TeX Stack Exchange site -- but which tend to be discouraged on most other Stack Exchange sites as far as I'm aware. But I assume it's mostly up to each individual site to define what makes a good question or good answer. (I want to check this assumption, hence the current question!)

As an example of the kind of resource I have in mind, consider this document on Github (brief extracts quoted below).

The file starts out by defining a "Hermetian Inner Product Space",

``````class herm_inner_product_space (V : Type u) extends vector_space ℂ V :=
(inprod : V → V → ℂ)
(is_fst_lin : ∀ (a b : ℂ), ∀ (x y z : V), inprod (a • x + b • y) z = a * (inprod x z) + b * (inprod y z))
(is_conj_sym : ∀ (x y : V), inprod x y = conj (inprod y x))
(is_pos_def : ∀ (x : V), (inprod x x).re ≥ 0 ∧ ((inprod x x) = 0 ↔ x = 0))
``````

It then defines (and proves) a bunch of lemmas. Its real objective, however, is to define the notion of Hilbert spaces, which it does at the end of the file:

``````class Hilbert_space (V : Type u) extends herm_inner_product_space V, uniform_space.core V :=
(is_open_uniformity : ∀s : set V, is_open s ↔ (∀x∈s, { p : V × V | p.1 = x → p.2 ∈ s } ∈ uniformity.sets))
(complete : ∀{f:filter V}, cauchy f → ∃x, f ≤ nhds x)
``````

What I'm suggesting is that the "question" in this case would look like this:

# Hilbert space

A Hilbert space H is a real or complex inner product space that is also a complete metric space with respect to the distance function induced by the inner product.

The entry `class Hilbert_space`... would ultimately become the "accepted" answer (✓). The other relevant items in the file would be alternative "answers".

To get this to work well, there should be tight integration with existing editors (e.g., Emacs, VS Code) so that it would be possible to download a given page and work with the contents offline. This way the formal mathematics could be checked interactively. The needed software integrations would be contributed by the user community (e.g., by me).

Comments on a given question and its answers would become inline comments in these exported files. Something would need to be sorted out about change management, e.g., I presumably shouldn't be able to directly change someone else's "answer", even if I find an error. Rather, I should upload an alternative version (like `Hilbert_space_bugfix1`). Usefully, we can tell whether an answer is "incorrect" by using the formal system to check it! Incorrect answers could be deleted by their authors or a moderator.

The advantages of co-authoring on Stack Exchange as opposed to working directly with Github are that each component of the file is easily discussable; small contributions can be made directly; people can get a kind of semi-tangible "credit" for their contributions. (Compare the definition of Commons-based peer production.)

The difficulties that I see would be minor technical ones. For example, file contents should probably appear in logical order rather than ordered by upvotes. However, that could presumably be arranged with a userscript, rather than requiring any server-side changes.

Naturally there's the question of achieving "critical mass", given that formalising mathematics is something of a specialist interest. However, the community is not tiny, either. Here's a group photo from a summer school in Cambridge last year that brought together many interested people: https://www.newton.ac.uk/event/bprw01/participants

If this isn't something suitable for Stack Exchange, then I think many of the same things could be done using OSQA. However, I expect that many users of the "Formal Math" site would also be contributors to math.stackexchange.com or Mathoverflow, and would appreciate having Stack Exchange as a one-stop shop for mathematics Q&A.

Would it be acceptable to set up the site here as an initial experiment?

• Regarding the basic metrics: questions per day: There are lots of mathematical objects and theorems out there that would need formalisation, and more every day as new papers come out. I think 10 questions per day would be pretty easy. answered: I expect that people in the user community would be willing to try submitting answers; the design whereby a lemma could be submitted as an answer would help. avid users and total users: The photo I linked to has ≈107 people in it. Not all would participate; some others might (e.g. students). We could get to 150. – Joe Corneli Aug 8 '18 at 16:06
• answer ratio: There would tend to be many "answers" per question, with one accepted answer. visits/day: I think we might struggle to get visits from non-users, but users would likely be pretty active. I think we might struggle some with this metric (1,500 visits per day is good; 500 visits per day needs some work. Eventually, 90% of a site's traffic should come from search engines.) -- but it's good to have something to struggle with. – Joe Corneli Aug 8 '18 at 16:10
• One further comment: there are already some questions about theorem proving systems on Stack Overflow (e.g., 1447 questions about Coq on Stack Overflow; 18448 questions about proof verification on math.stackexchange.com. These questions would be seen as "soft questions" on the "Formal Math" site; presumably such questions could be allowed, alongside actual formalizations) as a source of further documentation. – Joe Corneli Aug 8 '18 at 16:30