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:
Instead of a usual "question", each post would be a topic to formalize (e.g., "Hilbert space", "Fermat's Last Theorem").
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?
