mathematics free of a blackboard (I. Gelfand and M. Gromov)

[Josef Urban]

Voevodsky's Homotopy type theory (HoTT) seemed very much motivated by his
struggle with flexibly identifying different representations when he tried
proof assistants (PAs) in his math domain.

But people have been addressing similar things in various ways in PAs long
before him. Examples are the "smart" parsing mechanisms used by Gonthier in
the Coq formalization of Feit-Thompson, type classes and isomorphism
"transfers" in Isabelle, etc.

I am not saying that the formalization community has completely succeeded
in this - there is a long way to go. But Gromov seems to be throwing out
the "logic baby" (formal proof verification, automation, computation) with
the bathwater and quite unaware of the work of the PA community on such
topics.

Btw., I wrote this in 2009 (p. 23 of  https://arxiv.org/pdf/1109.3687v1 )
about Mizar's linguistic automation (which is so old that it predates type
classes in Haskell):

======
Mizar is in some sense both typed and untyped. In a narrow foundational
sense, Mizar is based on set theory, which is typically considered untyped.
The set-theoretical world initially consists of many objects of “just one
type”, in a similar spirit as the physical world initially consists of many
objects of “just one kind” (strings for example). These objects can have
various properties (a number, ordinal number, complex number, cardinal
number, Conway number, a relation, function, complex function, complex
matrix), however none of them is considered to be of “foundational
importance”, and all these properties are treated as equal “adjectives” or
“attributes”. Typically, mathematicians are interested only in some
particular properties of the objects, and fluently shift and focus between
them, and take some of them as granted in various contexts. Thus, the set
of natural numbers can once be treated as a measurable cardinal, another
time as a subset of real (and thus “obviously” complex) numbers, and
another time as a commutative semiring. The Mizar “typing” mechanisms are
concerned with providing such fluid and “obvious” treatment of the
adjectives. Note that recently similar automation mechanisms have been
added to other proof assistants, some of them based on (simple) type
theory, and sometimes such mechanisms have even been called “type
inference”. Examples are syntactic mechanisms like implicit coercions and
canonical structures in Coq, and type classes in Isabelle and Coq. We leave
it to the readers and their foundational beliefs and tastes to decide for
themselves what exactly counts as “type inference”, and instead focus on
explaining how these mechanism work in Mizar.
===========

Josef

On Thu, Mar 11, 2021, 23:21 José Manuel Rodríguez Caballero <
josephcmac at gmail.com> wrote:

> Ignacio wrote:
>
>> Your enhancement of the Pi calculus, as a first experiment to build a
>> programming algebraic language worthy of our intuitive grasp, looks
>> very important, I will look into it; but most of the work done in
>> proof assistants, seems closer to the knowledge realm, than to the
>> Reason sphere...
>
>
> After watching M. Gromov's lectures "Probability, symmetry, linearity," I
> changed my mind concerning proof assistants, including my prototype. Let's
> begin with his quote:
>
> We want mathematics free of blackboard, and it is impossible. We want to
>> verify mathematics in computers but this depends on the rigid structure of
>> computers and sometimes it fails. The great miracle of mathematics is
>> there. [...] All traditional descriptions of mathematics, in my view, are
>> greatly faulty, and this is the reason why there is no model of mathematics
>> realized in computers, why there is no model of understanding languages,
>> because we have an absolute wrong perception traditionally build in a
>> development of numerical mathematics in logic distorted our perception of
>> ourselves, of mathematics and of languages. It is as distorted as the Sun
>> orbiting the Earth, [...] it is the wrong language, the wrong description.
>
>
> M. Gromov, https://youtu.be/aJAQVletzdY?t=3880
>
> My interpretation of this statement is that expressions are like
> coordinate systems of a mathematical object. The same mathematical object
> can be represented in several ways, using different expressions. A trivial
> example is the number 2/3, which can be represented as 2/3, 4/6, 6/9, etc.
> One of I. Gelfand's famous quotes is:
>
> all of mathematics is some kind of representation theory
>
>
> This Gelfand's quotation is mentioned in this book: Huang, J.S. Lectures
> on Representation Theory; World Scientific: Singapore, 1999.
>
> Now, let's apply this idea to pi-calculus. Two pi-expressions are
> considered to represent the same process if and only if the structural
> congruence relates them. Hence, a process is not an expression in
> pi-calculus but a class of expressions corresponding to the structural
> congruence quotient. Here is a reference to pi-calculus:
>
> Milner, Robin. "Functions as processes." *International Colloquium on
> Automata, Languages, and Programming*. Springer, Berlin, Heidelberg, 1990.
> https://hal.inria.fr/inria-00075405/document
>
> To define computation from mathematics is questionable from an
> epistemological perspective since our direct experience is with computation
> (including measurement as a computation in the physical world), not with
> mathematics. Mathematics may be the result of abstraction in a computation.
> A mathematical object may not be a primitive concept but a concept derived
> from computation. The following argument seems to be a counterexample of
> this claim:
> from the premises:
>
> 1. Every language is an algebra
>> 2. There are several languages with subgroups unrelated to computation
>
>
> it can be possible to derive the conclusion
>
> L. Not every algebra is entirely for computation
>
>
> but rather than a counterexample, it is a positive example. Indeed, an
> algebra that is unrelated to computation is an abstraction from an algebra
> that is related to computation: this abstraction is obtained by ignoring
> the property of being computational.
>
> In this framework, it is rather natural to ask the following questions. I
> provided the answers corresponding to the particular point of view that I
> am following. Other researchers having a different point of view may
> provide different answers.
>
> Why mathematics is useful: The computational universe of computations at a
> maximum level of sophistication is reduced by identifying different
> expressions as representations of the same mathematical object. Mathematics
> is a trick to make shortcuts in irreducible computations. The price to pay
> for that is the loss of control over the representative of the mathematical
> object, e.g., one representative from one irreducible computation may
> transform itself into another representative to make a shortcut. Still, we
> are not in the original computation anymore.
>
> Why current proof assistants are a failure for everyday mathematics: In
> current proof assistants, a considerable amount of computational effort is
> used to change from one representation of a given mathematical object into
> another. In real-life, mathematicians consider all the representations
> simultaneously, i.e., in coordinate-free differential geometry.
>
> Here is an example of the effort needed to change from one pi-expression
> to another pi-expression in the formalization of pi-calculus in
> Isabelle/HOL:
>
> Bengtson, Jesper, and Joachim Parrow. "Formalising the pi-calculus using
> nominal logic." *International Conference on Foundations of Software
> Science and Computational Structures*. Springer, Berlin, Heidelberg, 2007.
> https://arxiv.org/pdf/0809.3960.pdf
>
> How to develop the first practical proof assistant: Using a mathematical
> model where the mathematical objects are treated in a way as independent as
> possible to their representation.
>
> The main difference between category theory and set theory is the
> foundations of mathematics: Category theory is about the mathematical
> objects, independently of the representations, whereas set theory is about
> the representations of the mathematical object.
>
> Kind regards,
> José M.
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210312/137b2361/attachment.html>