The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

"Name brand" mathematicians, just like physicists, computer scientists, and software engineers, only care about one thing: doing work which makes sense for their careers.

 

That may be true for most but should we just shrug our shoulders and accept it?

No; we should roll up our sleeves and embrace it.

It's all about the students. Pure math is a competitive career choice that (unlike comp sci) doesn't have a built-in backup job. Every generation of students is looking for a way to stand out. When blogging was new, the grad students started blogging. When math overflow was new, same thing. Same with Wikipedia, same with nLab. If you build new ways for people to contribute, you'll get new people and new contributions. Find ways to align your objectives with the needs of your audience.

"Hey, while you're reading that book, why not consider taking your notes in [Coq/Agda/Lean] and putting them up in [opam/whatever package manager]. Here's a link to a conference you can present that at. Here's a mailing list where people will appreciate your work. Here are some people in math departments who will talk to you about your project."

TLDR: if you want to change how people do things, you need to show them a better way

 

I mean is it not dangerous if we only follow one path where we know that there are several alternatives and dig one hole deeper without looking whether we dig in the right place?

Perhaps it is; but more importantly, the one-path mentality just doesn't match the actual phenomenology of modern math. Perhaps many mathematicians would put themselves in the ZFC camp as a kind of default/trained response; but I don't think many would deny that there is math outside of ZFC.

 

If as Kevin is saying Mathematicians get brainwashed in the beginning of the career to accept a certain style of Mathematics then maybe it is time to do something about this. And not just say this is how it is.

 

Maybe in the end Computer Science saves Mathematics.

I've read traditional math papers and I've read modern CS papers, and I have to say, "literate .v [.agda/.lean] is the new .pdf."

Adam Chlipala summarized the situation nicely in the 1st chapter of FRAP (http://adam.chlipala.net/frap/):

However,  we  follow  another,  much  less  usual  convention:  while  we  give  theorem and lemma statements, we rarely give their proofs.  The reason is that the author and many other researchers today feel that proofs on paper have outlived their usefulness. Instead, the proofs are all found in the parallel world of the accompanying Coq source code.

As the kids would say, "louder for the people in the back!"

 

 

Thorsten

 

 

From: <coq-club-request AT inria.fr> on behalf of Timothy Carstens <intoverflow AT gmail.com>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Thursday, 9 January 2020 at 00:37
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Fwd: "Lean is like Coq but better"

 

Kevin is deeper into the math world than I, but this matches my experience on all points.

 

"Name brand" mathematicians, just like physicists, computer scientists, and software engineers, only care about one thing: doing work which makes sense for their careers.

 

Strategic realism dictates that, if I saw a path towards proving the Jacobi conjecture, I would not bog myself down with constructive concerns unless I absolutely had to. Why would I? Even a proof-sketch would be enough to advance my career (perhaps even more-so than a completely worked proof!) Professional mathematics is a fundamentally social activity and "finished proofs" are more like milestones than atomic units of work.

 

There is an entrepreneurial angle to this thread that I think could be profitably recognized.

 

Suppose I'm in the business of building tools for metal working and machining. How can I win new customers? One method is to make incremental improvements to the state of the art: "This is a drill press. You already have a drill press, but this one offers better value over its lifetime. Your employees already know how to use a drill press, so it won't be much work to train them on how to use this new one."

 

Another method is to make changes to /the broader work process./ "This is a Foo and this is a Bar. They seem funky, but together, they replace your drill press, chop saw, and micrometer. Your employees have no clue how to use these things, your designers don't know how to design for them, and your project managers don't know how to plan timelines around them. But once they're trained, they'll be more efficient than people who are still using outdated drill/chop/meter tech."

 

Back to math, CS, and mechanized logic. Sometimes these discussions feel like an attempt to squeeze these new ideas into the 1st kind of pitch. "Dear mathematicians: your life will be the same as it is now, except that faulty proofs will be less common. The only price is, you need to revisit your notions of LEM and AC." I dunno man, hard sell.

 

If you want to pitch a new foundations [and as far as I can tell, *all* mechanized foundations are a "new foundations" relative to ZFC+pdf], I think you need to offer a bigger impact. What other parts of the mathematician's dayjob/ecosystem will be impacted?

 

I think we could learn a lot by talking to math grad students about these matters. When I was a grad student, I would have *loved* to live in a world where PDFs had hyperlinks to the relevant definitions. For example, a formal wikipedia+mathoverflow+arxiv mashup of some kind would have completely changed the grad student experience for me.

 

As to particulars of which logic with what properties, I suspect that different trades will continue to work in environments that are productive for their purposes.

 

It's almost as if we need a system which lets us define, study, and relate "domain specific logics," some kind of foundation beneath the foundation, some sort of ... meta-math perhaps ? :)

 

-t

 

 

 

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.