14
$\begingroup$

I'm interested in the machine translation of mathematics from informal to formal (a la Ganesalingam in The Language of Mathematics). As a first step, I am designing a computer language for expressing mathematical definitions, theorems, and arguments that would at some later point be amenable to a small formalization kernel. (At this point, the language looks like a pared-down Isabelle/ZFC with support for functions not defined on full domains, realm-like objects, and a weak sense of parametric types and polymorphic functions).

This translation project, which is already sizable, would be the first step towards making a general mathematical knowledge management system/formalization system. The goal of this system would be to be sufficiently useful and easy to use that it sees adoption by those who don't intrinsically care for formalization. Cf. this old MO post for previous community thoughts about such a system.

Recently, the system of univalent foundations by Voevodsky has brought general interest back into formalization. The system of univalent foundations, like the type theoretic conceit that "a proof is an instance of a proposition type" that univalent foundations is ultimately based on, is illuminating and quite beautiful, and I found my brain exploding repeatedly while reading the IAS book on the subject (available here).

Questions:

  1. Do univalent foundations provide a better structure for the introduction of definitions and the statement of theorems than the system I describe in the first paragraph? Can the intensional/extensional questions resolved by the univalence axiom in practice be handled by realms?

  2. If univalent foundations provides this better foundation, will users who try to understand definitions and theorems in this system necessarily need to understand univalent foundations?

  3. Which kinds of formal arguments are easier to make using univalent foundations, and are some kinds of sentence-by-sentence translations of informal proofs more feasible?

  4. Is full-scale reflection in the sense of John Harrison's Metatheory and Reflection in Theorem Proving able to introduce the advantages of univalent foundations into a less well developed underlying type theory?

I am working on this problem because it seems important and not because I am particularly suited for it, so any thoughts would be very helpful.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ This is an aside, I like your question, but it seems like you and Charles Wells might have a prolific conversation if you aren't already in touch. $\endgroup$
    – François G. Dorais
    Commented Nov 23, 2015 at 2:00
  • 2
    $\begingroup$ I would say that this question (#1), at present, is impossible to answer. Only until decent tools exist, and then a few thousand theorems [not lemmas!] are formalized will one know whether it is any good. And, of course, one will need to formalize a variety of mathematics. Analysis and geometry are considerably harder to formalize than algebra and combinatorics. And 'symbolic analysis', which first-year calculus students do all the time, has never been fully formalized! [C. Kaliczyk's thesis being an exception.] So we have no idea which system will be able to 'do mathematics' properly. $\endgroup$
    – Jacques Carette
    Commented Nov 23, 2015 at 22:23
  • $\begingroup$ But thanks for mentioning Realms! $\endgroup$
    – Jacques Carette
    Commented Nov 23, 2015 at 22:23
  • 1
    $\begingroup$ There was some discussion of this topic on the Foundations of Mathematics mailing list in October 2014. The Blakers-Massey theorem was cited as an example of something that is readily formalized in HoTT but possibly not so easily formalized in ZFC. Unfortunately you may have to wade through a lot of not-so-relevant discussion to find what you want, but here are two pointers: cs.nyu.edu/pipermail/fom/2014-October/018251.html cs.nyu.edu/pipermail/fom/2014-October/018283.html $\endgroup$
    – Timothy Chow
    Commented Nov 29, 2015 at 22:52
  • 1
    $\begingroup$ @MichaelBächtold cl-informatik.uibk.ac.at/users/cek/docs/09/… which is from his home page at cl-informatik.uibk.ac.at/users/cek. $\endgroup$
    – Jacques Carette
    Commented Oct 8, 2017 at 14:29

1 Answer 1

Reset to default
4
$\begingroup$

Regarding 2, structural set theory may be seen as a subtheory of the univalent foundations (Ch10 of the book, or our paper).

For 3, the nlab has a list of advantages.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .