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

Martin Escardo

@EscardoMartin

I would call this the First Law of Computer Formalization. The way the computer resolves the missing information should be guaranteed to be the same way as (educated) people using proofs assistants do.
15/

14/10/2022, 19:44:33

Favs: 8

Retweets: 0