philosophy: the immediate aspect of mathematics

Stream: general

[Johan Commelin]

Disclaimer IANAP (I am not a philosopher). But sometimes I like to dabble in it a bit. And it seems that the people at CMU have close ties to philosophy, so maybe they can help me out. Here is a proposition:

Pen and paper proofs destroy the immediate aspect of mathematics. Formally verified proofs in a computer proof assistant destroy it even further.

I'm probably not the first person with thoughts in this direction. If anyone has written something down about this, I'd be glad to be handed a pointer.
But I'd also be interested in a general discussion here on Zulip. All (un)thoughtful comments welcome!

[Kevin Buzzard]

What does "destroy the immediate aspect of mathematics" mean? This is not some trick question -- I just don't understand the phrase.

[Johan Commelin]

Well, when someone explains you a proof in person, there is this feeling that the ideas just flow towards you. When you read a pen and paper proof, you have to work a lot harder to "reconstruct" the actual maths. With a formal proof you are even further bound to some representation of the mathematics. But it is not the maths itself.
Something like the map is not the territory. Or the way a score is not the actual music.

[Johan Commelin]

Maybe I'm just discovering how much of a Platonist I am? I feel like formal proofs are tying maths down into the realm of bits and bytes... and that has been an itching me for a rather long time now

[Johan Commelin]

I wonder if people recognize that itch

[Johan Commelin]

@Kevin Buzzard In your MO answer to "What is a perfectoid space?" you say that a perfectoid space is a term of type PerfectoidSpace. And of course you meant it as a joke. But sometimes I fear that theorem provers would actually become common practice in maths departments, then your answer would cease to be a joke. And that feels wrong to me.

[Rob Lewis]

I'm also not really a philosopher, but I think you might be reaching toward what some people call "mathematical understanding." Talking about "actual maths," "maths itself," this is really hard to do without a lot of awkward metaphysical commitments. But the feeling of "ideas flowing toward you" is a little easier to get a grasp on.

[Rob Lewis]

The obligatory paper link is from our very own, of course. http://www.andrew.cmu.edu/user/avigad/Papers/understanding2.pdf

[Johan Commelin]

Thanks for the link

[Rob Lewis]

I think it explicitly avoids the metaphysical questions you're trying to ask.

[Johan Commelin]

The abstract is very interesting!

[Kevin Buzzard]

Yeah uncommented code is not written to be read. The big difference between talking to someone and reading a pen and paper proof is that talking to someone is a two-way thing so the explainer can adapt to the explainee. Sure formalising a proof destroys it even further. But putting comments in your code gets you to a state where you're better than a book, because now you're a book where people can right-click on what they don't understand.

[Rob Lewis]

I think most of the CMU-trained philosophers and "philosophers" would rather read your question as one about practice, instead of about real mathematical objects. How do we interact with mathematical concepts and explanations, and how does that interaction change when we read a formal proof vs an informal proof vs listen to a talk.

[Reid Barton]

Kevin Buzzard In your MO answer to "What is a perfectoid space?" you say that a perfectoid space is a term of type PerfectoidSpace. And of course you meant it as a joke. But sometimes I fear that theorem provers would actually become common practice in maths departments, then your answer would cease to be a joke. And that feels wrong to me.

I'm not sure whether this is what you're trying to get at, but I don't agree with "a perfectoid space is a term of type PerfectoidSpace". Rather, there's some "standard model" of Lean in set theory which tells us how to write down a particular set (which lives in the "actual mathematical universe") which corresponds to the type PerfectoidSpace, and a perfectoid space is an element of that set.

[Reid Barton]

In other words there's no shift in what a perfectoid space "is" (or a group, or a real number), we're just being much more precise in the kind of language we use, to the extent that even a computer can follow along.

[Reid Barton]

This seems related to your mention of Platonism, but less related to "ideas flowing towards you", etc.

[Reid Barton]

I do agree that as you pass from a heuristic argument to a proof sketch, to a proof, to a formalized proof, while you gain something at each step, you also lose something else.

[Kevin Buzzard]

It's a different kind of work recovering what you lost though, as you go from one way to the other. And if it's someone else's work I greatly prefer going from the formalised proof to the intuitive understanding, as opposed to wrestling trying to recreate the details of a sloppily-written paper that's done a great job of explaining the basic ideas and is now doing a crappy job of showing me the details. This might be personal taste though; I've always liked details and I've learnt that not everyone is like that.

[Reid Barton]

It's hard to say exactly what it is that is lost, but I think the proposition is still testable: a proof that's more "fully realized" tends to be harder to understand (for someone with the appropriate expertise), if only because it's longer, and harder to adapt to other settings

[Johan Commelin]

Thanks for the comments so far! I feel like I don't really have the language yet to express my thoughts. Also my thoughts are still very messy. But these comments are helping me in the right direction.

[Andrew Ashworth]

At least in computer science, I have come around to wanting well-commented code rather than a high level description of any given algorithm. I have spent so much time trying to recreate details lost in papers; and while I understand that a brief pseudocode description is more terse it's utterly useless if you actually want to use a result, which is the end goal (hopefully).

[Reid Barton]

What do you mean by "use a result"?

[Reid Barton]

Do you mean, actually implement and run on a physical computer?

[Andrew Ashworth]

Get actual running code that I can apply to whatever problem I'm trying to solve

[Reid Barton]

As far as I can see, this doesn't really have an analogue in math

[Andrew Ashworth]

I've been burned multiple times reading signal processing papers that promise a great new algorithm for doing something, but the performance improvement is only theoretical or only applies to a certain dataset that is not like my own data in some way.

Yes, I don't know if it's really analogous in math.

[Andrew Ashworth]

Do people often read mathematical papers that promise a great new technique or refinement of an approach, then try to apply it and get lost in the details, perhaps finding it's not applicable?

[Johan Commelin]

Not really in the way you were describing, I think

[Johan Commelin]

Although we certainly can get lost in details

[Johan Commelin]

But we can also choose to ignore them when things get murky

[Johan Commelin]

Just the same way you could ignore division_by_zero errors in your code. If you run a/random_int(10^6) it will only fail once in a million times. Who cares? :boom:

[Johan Commelin]

If only one in a million proofs are broken? Who cares?

[Rob Lewis]

Just the same way you could ignore division_by_zero errors in your code. If you run a/random_int(10^6) it will only fail once in a million times. Who cares? :boom:

Please never write airplane software, Johan!

[Reid Barton]

I think "technique" is being used in different senses. It sounds like you're using "technique" in the sense of algorithm--let's say a paper presents a new algorithm for sorting. We already knew we could sort lists, but here is another way to do it.
In math, this should correspond to a new proof of a theorem. But in math, from a logical point of view, a proof is always "applicable"--either the theorem is true or it's not, and if it's true, then as long as the hypotheses of the theorems hold, we can apply it. There are no considerations like "performance improvement".
Thus, in math, the value of a new proof of a known theorem is in understanding the ideas that went into the proof. From a practical standpoint, this means being able to reuse those ideas to prove new theorems. This is roughly what we mean by "technique".
In CS, the best example of this kind of technique that I could come up with is dynamic programming.

[Reid Barton]

Anyways, I was specifically not arguing that some points on this spectrum are better than others. Different points are better for different purposes. Best would be to have multiple points of view on "the same proof" (whatever that means). I think you get at this with your "well-commented code". Suppose your options were pseudocode in a paper or a 10M binary blob--then your preference would depend on the situation, surely?

[Reid Barton]

(And let's suppose the 10M code blob also comes along with a 100M blob that is a formal proof of correctness of the code.)

[David Michael Roberts]

There are no considerations like "performance improvement".

well, there was the SAT proof of one special case of the Erdős discrepancy problem, and there was the proof by Terry Tao. The methods that Tao employed came from other proofs that allowed a much better proof of the special case that some giant SAT certificate.

[Anthony Bordg]

Disclaimer IANAP (I am not a philosopher). But sometimes I like to dabble in it a bit. And it seems that the people at CMU have close ties to philosophy, so maybe they can help me out. Here is a proposition:

Pen and paper proofs destroy the immediate aspect of mathematics. Formally verified proofs in a computer proof assistant destroy it even further.

I'm probably not the first person with thoughts in this direction. If anyone has written something down about this, I'd be glad to be handed a pointer.
But I'd also be interested in a general discussion here on Zulip. All (un)thoughtful comments welcome!

Hello Johan,

you may be interested in my article, in particular section 3.
@Johan Commelin

[Johan Commelin]

@Anthony Bordg Thanks for the link, I'm putting it on my reading list.

[Johan Commelin]

The previous suggestion by Rob (Jeremy's article) was also a big success. I very much enjoyed reading it

[Jeremy Avigad]

I'm blushing.