🌗 《費馬最後定理專案》
➤ Formalisation of mathematics and Fermat's Last Theorem Project
✤ https://leanprover-community.github.io/blog/posts/FLT-announcement/
本文討論費馬最後定理的證明project， Kevin Buzzard 採取Leancommunity blog文章，探討費馬最後定理在數學中的重要性和挑戰，並介紹了formalisation of mathematics的概念。
+ 這篇文章讓我感到驚奇的是，費馬最後定理專案的目的是不是隻證明這個定理，而是形式化mathematics 的概念，以便computer scientists 可以幫助mathematicians 做研究。
+ 本文也討論了formalisation of mathematics 的重要性，讓我感到興趣的是，這個project 可能會在未來幫助computer scientists
#數學 #計算機科學 #Formalisation of mathematics

Comment la #formalisation peut-elle enrichir notre compréhension de processus historiques? À partir du cas de l'#épuration dans le monde du #spectacle, l'historienne Karine Le Bail et le mathématicien Julien Randon-Furling déploient, pas à pas, une analyse collaborative d'un mode de #justice spécifique.

👉 L’épuration professionnelle du monde du spectacle à la Libération. #Histoire et sciences #mathématiques

➡️ https://www.cambridge.org/core/journals/annales-histoire-sciences-sociales/article/abs/lepuration-professionnelle-du-monde-du-spectacle-a-la-liberation/BE7B542A4A08AD7DD09BB7120762C20C
➡️ https://www.cairn.info/revue-annales-2023-4-page-657.htm

@histodons #histodons #methodes

The British Nationality Act As a Logic Program
(1986) : Sergot, Marek J et al
DOI: https://doi.org/10.1145/5689.5920
#__important #formalisation #law #UK #nationality #prolog #logic #british_nationality_act #my_bibtex

Formalization of a voting protocol for virtual organizations
(2005) : Pitt, Jeremy V. et al
DOI: https://doi.org/10.1145/1082473.1082530
#formalisation #event_calculus #voting #MAS #protocol #organisation #my_bibtex

Expressive Equivalence of Planning Formalisms
(1995) : Bäckström, Christer
DOI: https://doi.org/10.1016/0004-3702(94)00081-b
#STRIPS #formalisation #expressivity #planning #ESP_reduction #my_bibtex

[ 🔄 ]

@Khrys 🔗 https://mamot.fr/users/Khrys/statuses/108573507916661072
-
#Police nationale: la Cour des comptes se paie le logiciel #Scribe

https://www.liberation.fr/societe/police-justice/police-nationale-la-cour-des-comptes-se-paie-le-logiciel-scribe-20220701_GEZJEY35GNFEDAKT7CMT7CH6VY/

Serpent de mer de la logistique #policière, le #logiciel Scribe a déjà coûté plus de 13 millions d’euros pour ne jamais voir le jour. Un #échec dû à «une absence de #cadrage», «une #formalisation très insuffisante de l’expression des besoins» et à «une absence de #contrôle à tous les niveaux» selon un #rapport de la Cour des comptes.

https://mstdn.jp/media/fsk51tfqvQqw2Ykb6qo

A talk by Kevin Buzzard of the Imperial College London: "Is HoTT the way to do mathematics?"

https://www.youtube.com/watch?v=q5-pykbfViA

He discusses criteria for a proof assistant to have in order to be used in formalising mathematics. Most mathematicians today assume classical logic and the axiom of choice.

#HoTT #constructive #cubical #typetheory #Agda #mathematics #formalisation