Martin Escardo

@EscardoMartin

Is this too outrageous?
1/

14/10/2022, 19:03:00

Favs: 22

Retweets: 7

Martin Escardo

@EscardoMartin

Foundations currently emphasize precision and consistency. But there is scope for "practical foundations" that additionally address how mathematicians (of all kinds!) actually do and write mathematics.
2/

14/10/2022, 19:03:00

Favs: 17

Retweets: 2

Martin Escardo

@EscardoMartin

In particular, this matters regarding how mathematical structures are organized.
(Groups, topological spaces, categories, graphs, posets, metric spaces, schemes, toposes, and much more.)
3/

14/10/2022, 19:03:01

Favs: 9

Retweets: 0

Martin Escardo

@EscardoMartin

For maths done on paper, this doesn't matter. Mathematicians and their students can sort this out in their heads, with no ambiguity. Maybe after long conversations, but still.
4/

14/10/2022, 19:03:01

Favs: 8

Retweets: 0

Martin Escardo

@EscardoMartin

But with the rise of proof assistants, which check your definitions and proofs, such conversations are not available.
5/

14/10/2022, 19:03:02

Favs: 6

Retweets: 0

Martin Escardo

@EscardoMartin

The proof assistant cares about precision *only*.
6/

14/10/2022, 19:03:02

Favs: 6

Retweets: 0

Martin Escardo

@EscardoMartin

There are some attempts to make the proof assistant to care about "practical foundations". Such as type classes and instance arguments.
7/

14/10/2022, 19:03:03

Favs: 6

Retweets: 0

Martin Escardo

@EscardoMartin

But I don't think (7) reflects how (i) mathematicians think about the problem, and (ii) how they resolve it in their written prose.
8/

14/10/2022, 19:03:03

Favs: 6

Retweets: 0

Martin Escardo

@EscardoMartin

Designers of proof assistants should pay more attention to how mathematicians think and write about what they think.
9/

14/10/2022, 19:03:04

Favs: 10

Retweets: 2

Martin Escardo

@EscardoMartin

Perhaps some people would say that the above "practical foundations" amount to the same thing as software engineering. Perhaps.
10/

14/10/2022, 19:03:04

Favs: 6

Retweets: 0

Martin Escardo

@EscardoMartin

But it has to be taken into account that the modes of expression that mathematicians have devised over centuries are successful for written-down, published, mathematics.
11/

14/10/2022, 19:03:05

Favs: 6

Retweets: 0

Martin Escardo

@EscardoMartin

I would like to see such modes of expression to be undertood and accepted by computer proof assistants. 12/

14/10/2022, 19:03:06

Favs: 4

Retweets: 0

Martin Escardo

@EscardoMartin

In a principled way.
13/

14/10/2022, 19:05:56

Favs: 5

Retweets: 0

Martin Escardo

@EscardoMartin

The most important thing is that statements of theorems are absolute clear to human readers. If unspecified resolutions of things (such as the meaning of "+") are present in the formulation of the theorem, a paper is not publishable on the grounds that it has been formalized.
14/

14/10/2022, 19:40:28

Favs: 4

Retweets: 0