[SystemSafety] Logical difficulties in mathematics

[David MENTRÉ]

Dear Mr Jones,

Le 15/02/2019 à 15:07, Derek M Jones a écrit :
> Publicity of problems and inconsistencies in code is spreading
> to mathematics.  Mathematicians are starting to highlight these
> issues in their field:
> https://njwildberger.com/2012/10/13/the-problem-of-rigour-in-modern-mathematics/
>
>
> Perhaps somebody ought to tell mathematicians about formal methods.

Isn't your remark out of scope for System Safety? Anyway, some
mathematicians know well about formal methods. For example there is
Voevodsky et al. work on Homotopy type theory that tries to rebuild
Mathematics on new grounds. This work is tightly tied to Coq proof
assistant.

  https://homotopytypetheory.org/book/


For more "classical" use of formal methods in Mathematics, you can look
at Gonthier et al. proof of 4 colours theorem
(https://www.ams.org/notices/200811/tx081101382p.pdf) or Gonthier et al.
proof of Feit-Thompson Odd Order Theorem
(https://hal.archives-ouvertes.fr/hal-00816699/). Beyond the
demonstration of those theorems, those works built a huge work of
formalized Mathematics in a mechanized way using Coq proof assistant
(https://github.com/math-comp/math-comp).

Sincerely yours,
D. Mentré