Revue MaSciProûve

Editeur responsable: Roland Coghetto

ISSN (Version imprimée) : 2795-9090

ISSN (Version numérique) : 2795-9104

Pour nous contacter:
Adresse numérique de la Revue MaSciProûve:	masciprouve (l'arobase) cafr-msa2p.be
Récupération de la clé publique:	gpg --locate-external-keys masciprouve (l'arobase) cafr-msa2p.be
Empreinte numérique de la clé publique:	83ED F155 6608 EFC7 DC98 ED87 B629 7BCE C2C3 E038

Téléchargements (Version numérique - pdf):

Au sommaire de ce numéro:

• Un peu de musique
  • Une approche géométrique avec MIZAR
  • Une approche arithmétique en Isabelle/HOL
  • Et si on écoutait notre musique avec CSOUND ?
• Dessiner dans le plan hyperbolique de Beltrami-Klein
  • L’approche métrique
  • L’approche géométrique
  • Equivalence de la distance suivant l’approche métrique ou l’approche géométrique
  • Cercle dans le plan hyperbolique de Beltrami-Klein
  • GCLC : Intersection des médiatrices d’un triangle : orthocentre ou intersection imaginaire de droites parallèles d’un faisceau ?
• Points intérieurs d’un triangle
  • Geometry Expert - Le théorème de Viviani
  • Formalisation du point intérieur à un triangle
  Il faut qu’on en parle...
  • Quelques disgressions sur la notion de type
    • Commençons par les ensembles
    • Poursuivons par un tout petit peu de théorie des catégories
    • Et terminons par un tout petit peu de théorie des types simples
• Références
• Annexes
  • Gamme pentatonique pythagoricienne/majeure
  • Cercles hyperbolique dans le modèle Beltrami-Klein
  • Code GCLC - plan hyperbolique (modèle Beltrami)

Au sommaire de ce numéro:

• Un peu de surréalisme avec les Chevaliers et les Valets
• Automatiques : CRC-24, SPARK et CVC5

Au sommaire de ce numéro:

• Classement par ITP
• Classement par ATP
• Classement par Bibliothèque
• Classement par Logique
• Classement par Matière
• Classement par Niveau
• Classement divers
• Bibliographie

Au sommaire de ce numéro:

• Errata
• Vous prendrez bien un peu de Lean ?
  • Installation classique
  • Première approche
  • Deuxième approche
  • Sur les univers
  • Les filtres
  • Plus facile d'accès...
  • Un service Web utile
• Trigonométrie
  • Méthodologie
  • Exemple 1
  • Exemple 2
  • Exemple 3
  • Exemple 4
• Lean... avec Emacs
  • Avec Mathlib4
• Un peu de Lean-géométrie...
  • Exemple
  • Première tentative
  • Seconde tentative
  • Troisième tentative: avec structure
  • Quatrième tentative: avec Class
  • Cinquième tentative: avec structure
  • Sixième tentative: avec Class
  • Septième et dernière tentative: avec structure
• L'assistant de preuve Rzk
• Il faut qu'on en parle

Au sommaire de ce numéro:

• GTARSKI,Formalized Mathematics et Metamathematische methoden in der geometrie : définitions et notations
• GTARSKI,GeoCoq et IsaGeoCoq : Définitions et notations utilisées
• GTARKI et IsaGT : Définitions et notations utilisées
• Géométrie neutre : construction de Gupta de la perpendiculaire à une droite passant par un point
  • Représentation graphique d'une perpendiculaire passant par un point dans le modèle cartésien
  • Représentation graphique d'une perpendiculaire passant par un point dans le modèle plan de Beltrami-Klein Construction d'une perpendiculaire passant par un point dans un modèle du plan projectif
• Quelques représentations graphiques dans le plan Beltrami-Klein
  • Construction du lieu des points équidistants à 2 points donnés
  • Construction de quelques figures symétriques
  • Quelques constructions approximatives de points équidistants à un point donné
  • Figure 13
  • Figure 16
• Code source
  • org.ads
  • org-beltrami.ads
  • org-beltrami.adb
  • test.adb

Au sommaire de ce numéro:

• Et si on lisait du code ?
  • statement69
  • hyp2.A3'
  • real_hyp2_B_hyp2_ctln2
  • real_hyp2_C_hyp2_ctln2
  • hyp2.A2'
  • hyp2_extend_segment_unique
  • Quelques visuels approximatifs possibles
  • Une lecture possible de cette démonstration formelle
  • Et si on changeait de langage : Mizar ?
  • Explorons la proposition statement69
  • Challenges
• Ensembles et classes
• GeoLean
• Isabelle/HOL : 'pour tout' local ou global ?
• Il faut qu'on en parle...

Au sommaire de ce numéro:

• Mizar in Rust
• Installation
• Utilisation élémentaire
• MEGALODON
  • Présentation
  • Licence
  • Installation de Megalodon 1.12
  • Exploration/réécriture de code
    • Section globale 1
    • Eq
    • FE
    • Ex
    • Section globale 2
    • PropN
    • SepSec
    • Section globale 3
  • 100thms_12.mg
  • challenges
• Mizar : Renommer les labels d'un article
• IsaGT : GTARSKI de Mizar vers Isabelle/HOL
  • Introduction
  • Des challenges
  • Le code complet
• Il faut qu'on en parle...

Au sommaire de ce numéro:

• Exemples
• Résolution classique
• Evaluation de solutions avec Maxima
• Avec Mizar
• Le contexte
• Question 1
• Question 2
• Question 3
• Question 4
• Avec Isabelle/HOL
• Question 1
• Question 2
• Question 3
• Question 4
• Exercices supplémentaires
• Question
• Pour aller plus loin...
• Annexes
• Code source Mizar
• Code source Isabelle/HOL

Au sommaire de ce numéro:

• Rendre une partie de preuve un peu plus compréhensible
• Comprendre les éléments de preuve
• De la formalisation en 4 problèmes de géométries élémentaires
• Premier problème
• Deuxième problème
• Troisième problème
• Quatrième problème
• Quelques pistes
• Quelques challenges...
• SMT : Une trop courte présentation
• Mizar est dans la boite : un raspberry pour vérifier des calculs ! (niveau école primaire ou adultes en alphabétisation)
• Introduction
• Calcul
• Calcul de système métrique
• Calcul horaire (et durée)
• Déroulement possible
• Présentation
• Un dispositif sur Raspbery PI 2
• Pour aller plus loin...
• Pour améliorer un peu ? Des challenges en vues...
• La place de l’ordinateur à l’école primaire

Au sommaire de ce numéro:

• Le code source de Mizar est rendu public sous GNU GPLv3
• Installation de Mizar sur Raspberry PI
• Introduction
• Prérequis
• Installation
• Remarques
• Vérification partielle ou totale de la Mizar Mathématical Library MML
• Exercice de Géométrie élémentaire avec IsaGeoCoq2_R1
• Solution et généralisation de l'exercice 21 de "2000 Théorèmes et Problèmes de Géométrie avec Solutions"
• Trisection d'un segment - Gamme pentatonique et heptatonique pythagoricienne
• Le centre de documentation
• "2000 Théorèmes et Problèmes de Géométrie avec Solutions"
• Instruments de musique en papier et carton
• Annexes

Au sommaire de ce numéro:

• Interview de M. Pascal Fontaine - WG Automated theorem provers - CA20111 - Suite et fin
• Les ensembles
• Mizar et les polynômes
• Annexes
• Codage d'Ackerman
• Solution(s) des exercices

Au sommaire de ce numéro:

• Les démonstrateurs automatiques de preuves
  • Prover9
  • MizAR
• Le coin des logiciels
  • TPTP
  • 17 marteaux assistants automatiques de preuve
• Le coin des bibliothèques
  • Mizar Math Library (MML) / Isabelle/ZF
  • Isabelle/Hol: NSA
• Il faut qu'on en parle
  • Mathématique moderne et bibliothèques numériques des assistants de preuves
• L'association sur internet
• Le centre de documentation
  • "L'éducation postmoderne"

Au sommaire de ce numéro:

• Erratum
• Le coin des logiciels
  • Agda
  • cooltt
  • Coq
  • Isabelle
  • HOL Light
  • Lean
  • Megalodon
  • Metamath
  • Mizar
  • Lambdapi
  • PVS
• Le coin des bibliothèques
  • Bibliothèque - Agda
    • agda-algebra
  • Bibliothèque de logique floue - Mizar
  • Des nombres complexes à partir des nombres surréels: une expérimentation avec Megalodon
• Il faut qu'on en parle...
  • Les bibliothèques et la gestion des versions des logiciels
  • HOL et les axiomes ZF - un point de vue en Metamath
• L'association sur internet
• Le centre de documentation
  • "La logique floue et ses applications"

MaSciProûve Vol. 1 Num. 2 (Avril - Mai - Juin 2022)

Au sommaire de ce numéro:

• Le coin des logiciels
  • GCLC
    • Théorème de Pappus
    • Trisection d'un segment
• Le coin des bibliothèques
  • Bienvenue dans la Matrix...
  • Le théorème de Fubini, Version Mizar
• Il faut qu'on en parle...
  • La Géométrographie
    • Recueil en ligne de problèmes de construction de positions triangulaires
    • Sur l’automatisation des constructions de triangles en géométrie absolue et hyperbolique
  • Isabelle dans la matrix...
• Interview de M. Pascal Fontaine - WG Automated theorem provers - CA20111
• L'association sur internet
• Le centre de documentation
  • "La convivialité"

MaSciProûve Vol. 1 Num. 1 (Janv.-Févr.-Mars 2022)

Au sommaire de ce numéro:

• Le coin des bibliothèques
  • GeoCoq: Varignon
  • Mizar Mathematical Library (MML): Topologie
• Il faut qu'on en parle...
• Le centre de documentation
  • "La logique pas à pas"
  • "Eléments de logique"

Adresse électronique de la revue: m a s c i p r o u v e [at] cafr-msa2p.be