[FOM] Improving Set Theory

[José Manuel Rodríguez Caballero]

Kevin Buzzard wrote (quoted by Tim):
The HOL systems can only take you so
> far because simple type theory does not seem to me to be strong enough
> to do modern mathematics in a convenient way

That depends upon the part of modern mathematics in which a concrete
mathematician is working. For example, I learned Isabelle/HOL in a
self-taught way and I formalized nontrivial theorems in number theory [1] ,
some of them were classical results, some of them, my own theorems, related
to my publications on a subject that I call the language-theoretic approach
to number theory (for example, [4]).

Currently, I am working with Dominque Unruh in the formalization of
functional analysis, including the tensor product of Hilbert spaces [2]. I
do not see any serious difficulty in Isabelle/HOL beyond the difficulties
of ZFC.

  Kevin Buzzard wrote (quoted by Tim):
, although note that
> Isabelle/HOL and perhaps other HOL systems have a healthy amount of 19th
> century analysis (e.g. Dirichlet's proof of infinitely many primes in an
> AP).

All my formalizations with Unruh in [2, 3] are XX century mathematics and
some of the results of [1] are XXI century mathematics (my own
publications).

I have no idea what are the axioms of simple type theory, nevertheless, I
was able to formalize several theorems in Isabelle/HOL, because the
mathematical intuition is the same and the artificial intelligence
(sledgehammer) fills the details in simple type theory.

I think that the main problem with proof assistants in mathematics (in
contrast to engineering) is that most people using them have been trained
as computer scientists and not as professional mathematicians. So, when
they try to formalize a mathematical theory that they do not understand, it
is hard for them to even to copy the proof from a textbook. Of course,
there are exceptions: computer scientists who are also mathematicians in
spirit for which this remark does not apply.

Kind Regards,
José M.

[1]
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory/tree/Dyck-(old-version)

[2] https://github.com/dominique-unruh/tensor-product

[3] https://github.com/dominique-unruh/bounded-operators

[4] http://math.colgate.edu/~integers/u2/u2.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200114/2a0aed03/attachment-0001.html>