The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Call me naïve but I thought we are talking about science.  

 

"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? 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?

 

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.

 

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.