I think the key step that needs to be done is to start to teach mathematics using proof assistants similarly to how the Software Foundation initiative does it for programming languages.

It may be at first a graduate course in constructive mathematics e.g. in constructive algebra.

Due to the way the motivational structure of mathematical learning is organized it would be very good and may even be necessary for such a course to succeed to have several unsolved *conjectures* or *problems* to attract students.

I know of one such problem - to find a constructive proof of Merkurjev-Suslin theorem about K_2/l . Constructive here might mean simply a proof that does not use the axiom of choice but I believe that to find such a proof one has to learn real constructive algebra such as the constructive description of the algebraic closure of a field (one can assume that it has decidable equality).

I also believe that finding a constructive proof pf this theorem will open the way to the correct formulation and proofs of many questions related to the structure of Galois cohomology that we at the moment have no idea how to approach. 

I have a feeling that there are also many such questions in number theory where having a constructive proof would mean achieving a much higher level of understanding of the structures involved and ultimately to the solutions of problems that are open in classical mathematics.

Vladimir.






On Jun 12, 2016, at 4:20 PM, James Cheney <james....@gmail.com> wrote:

Hi Andrej,

This is a problem in many scientific disciplines, not just (formalized) mathematics.  It is beginning to be understood that software development and maintenance needs to be recognized as a scholarly activity in order to make it more likely that software needed to reproduce and understand research results is available and preserved

https://figshare.com/articles/There_s_No_Such_Thing_As_Irreproducible_Research_Software_Credit_Edition_/3159295/1

and in the UK at least, the Software Sustainability Institute is trying to support scientists in a range of disciplines to develop better software:

http://software.ac.uk/

Also in the UK, the Alan Turing Institute is supporting "research software engineers" whose job it will be to turn promising researchware developed by ATI fellows/students into reusable/documented/tested packages.  So far it seems that the powers that be view the ATI as primarily about big data and machine learning, though.  The UK has no analogue to INRIA, nor the US as far as I know; I think the closest analogues are the national labs but (at least w.r.t verification and formalized mathematics) they are much less visible than INRIA. 

It would be great to put the problems of formalized mathematics in the picture for such organizations.

In addition to the recent Coq-related efforts mentioned by others, one should consider the Isabelle/HOL and ACL2 communities. Isabelle/HOL does get used in industry, e.g. NICTA/Data61's formalization of sel4 kernel.  See talks by J Moore on ACL2 and by Gerwin Klein on sel4 at the recent Royal Society discussion meeting on "verified trustworthy software systems"

https://royalsociety.org/events/2016/04/software-systems/

There are also (relative) success stories in mathematics, e.g. the GAP system:

www.gap-system.org/

None of this is to say that software credit and maintenance (and development to the level of maturity needed for acceptance in the mathematical community) is a solved problem, but there are other solution attempts that can be considered to better understand the problem.  Fundamentally, what is needed is resources, whether this means money from funding agencies, investment capital, or donations of free time from open source contributors. In each case, persuasion and leadership is needed, but what form this takes seems very situation-dependent and there is no guarantee that the needed model will fit anyone's pre-existing vision of a "successful [academic] career".

--James

PS. I also enjoyed the comic.


On Sun, Jun 12, 2016 at 9:28 AM, Andrej Bauer <andrej...@andrej.com> wrote:
On Sun, Jun 12, 2016 at 10:04 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> http://www.smbc-comics.com/index.php?id=4127

And now for something completely different:
http://wstein.org/talks/2016-06-sage-bp/bp.pdf

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.


--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.