cafr-MSA2P asbl

Bienvenue sur le site web de l'association "Centre autonome de formation et de recherche en mathématiques et sciences avec assistants de preuve" asbl (non-profit organisation) (cafr-msa2p)

Pour en savoir plus sur les assistants de preuves:

Assistant de preuve (en français, Wikipedia)

Les assistants interactif de preuve

Théorie des ensembles (en français, Wikipedia)

Théorie des ensembles Tarski Grothendieck (en anglais, Wikipedia)

Théorie des types (en français, Wikipedia)

Les assistants automatiques de preuve

Une liste d'assistant de preuve (en anglais, github)

Une liste de 100 théorèmes formalisés ou à formaliser (en anglais, site de Freek Wiedijk)

Séminaire Bourbaki - 21/06/2014 - 4/4 - Thierry Coquand

How to Do Maths Wihtout Depent Types - Anthony Bordg (20 juin 2022, Conférence IHES, en français)

Pour en savoir plus sur l'association:

Pourquoi ce nom « cafr-msa2p » d’association ? C’est incompréhensible ?!
Oui en effet, « GUITP du Centre » (« Groupe d’utilisateurs d’ITP de la région du Centre »), comme par exemple « LUG » (Linux User Group) ou « Coding Dojo Centre », aurait été plus sympa mais pas très visible ni compréhensif pour le public. En effet, comme il n’existe, à notre connaissance, aucun groupe de ce type, nous avons voulu être plus explicite.
Pourquoi alors « Centre autonome de formation et de recherche » et pas « Groupe d’utilisateurs... » ?
Nous espérons que la notion de « Centre » permettra de rassembler les initiatives en un lieu plus visible et de permettre l’accueil à toute personne intéressée par le sujet. Après une mode à la décentralisation systématique (forum, groupe, blog, réseau sociaux) qui a des avantages indéniables, il nous paraît aussi important de partager un lieu central de rencontres et de partages.
Nous revendiquons la notion d’« autonomie » : les décisions ne sont pas liées à des dons (un assistant de preuve peut nous sponsoriser mais nous sommes pas tenus de défendre sans réserve ou d’utiliser uniquement ce logiciel).
Même si nous avons comme objectif de promouvoir ces logiciels et bibliothèques associées, nous ne sommes pas lobbyistes auprès de l’UE (voir à ce sujet lobby-groups).
« Centre autonome de formation et de recherche »… L’association est-elle attachée à une Haute École, affiliée à une Université ou au FNRS ?
Non pas du tout. Il s’agit d’une initiative privée.
L’association délivre-t’elle des diplômes ou des certificats ?
Nous ne délivrons pas de diplômes. D’ailleurs, en Belgique francophone (Communauté française), seules les établissements d’enseignement supérieur [. . .] sont habilités à délivrer les titres, grades académiques, diplômes et certificats correspondant aux niveaux 5 à 8 du cadre francophone des certifications.” (cf. Art. 3 §3. du Décret définissant le paysage de l’enseignement supérieur et l’organisation académique des études).
Nous ne délivrons pas de certificat de formation.
Organisez-vous des cycles de formations ?
Non. Il n’y a pas de formation du type « formation niveau 1 pour débutant », « formation niveau 2 » etc.
Nous privilégions les échanges d’informations, de points de vue entre membres, leur compétences.
En terme de formation, nous privilégions, par exemple, la réalisation d’un chef d’œuvre qui sera diffusée dans la revue interne à l’association MasciProûve et le code créé mis-à-disposition de la communauté sous forme de licence libre. « La réalisation d’un Chef-d’œuvre (personnel ou collectif) est une pratique qui s’inscrit parfaitement bien dans le cadre du travail social. Elle invite les participants à concrétiser et à mettre en valeur leur savoir ainsi qu’à prouver leurs capacités. Elle les stimule à se surpasser dans une production qui sera exposée et/ou diffusée et qui donc devra présenter une qualité certaine. L’essentiel ici est que l’entreprise soit un succès, ce qui changera l’image que la personne a d’elle-même parce que le regard de l’autre aussi aura changé ». Jean-Pierre Pourtois et Hughette Desmet in « L’éducation postmoderne », 1997.
Vous faites de la recherche ?
L’association s’insère dans la production d’articles scientifiques (Formalized Mathématics (Mizar)) ou de depot (Archive Formal Proof)
Il est important de montrer que la recherche scientifique est aussi accessible, dans ce domaine, à des hobbyistes amateurs. Nous n’avons pas les mêmes moyens que des membres d’Université ou de centre de recherche nationaux.
Nos réalisations (également en collaboration):
- 23-24 September 2022: EuroProofNet workshop on the development, maintenance, refactoring and search of large libraries of proofs, Tbilisi, Georgia
  
  Roland Coghetto and Julien Narboux (University of Strasbourg) [online], The GeoCoq library and its porting to Isabelle – Présentation de Julien Narboux
  "GeoCoq is a formal proof library consisting in a formalization of foundations of geometry. It is based on several different axiom systems by Euclid, Hilbert and Tarski, and includes the arithmetization of geometry, i.e. the link between synthetic and analytic geometry. After giving a quick overview of the library, we will discuss how automation and logical foundations are used in each part of the library and the potential impact on porting the library to other proof assistants. Then, we will report on the porting of the library to Isabelle/HOL by Roland Coghetto."
  (Program,Slides)
- Revue « Formalized Mathematics »
  Publications :
- Revue «Mechanized Mathematics and Its Applications, Works in Progress (MMA-WiP) »
  - MMA-WiP (2022), vol. 4, no.1:« Highschool (Secondary School) Trigonometry: Some Exercices with Mizar} », Roland Coghetto

Nos recherches en cours:

IsaGeoCoq2_R1 en Isabelle/HOL sur github ou sur notre serveur
GTARSKI_5 (Mizar) (Voir: En relecture)
Modèle Beltrami-Klein Mizar
La trigonométrie avec l’assistant interactif de preuve Mizar
Découverte et exploration de Lojban - Mizar

L’association organise-t’elle des stages d’initiation ?
Pas pour le moment.
Faut-il déjà connaître les assistants de preuve ?
Non vous êtes le bienvenu, même si vous ne connaissez pas les assistants de preuve.
Je suis passionné(e) par ce sujet et je veux en faire mon métier ! Super je viens chez vous ?!
Vous êtes le/la bienvenu(e). Néanmoins, vous êtes responsable dans le choix de vos études. Nous vous conseillons de vous inscrire dans une Haute-Ecole ou Université. Dans la mesure de nos moyens, nous pouvons vous accompagner pour la prise de contact avec le monde de l’Enseignement supérieur ou Universitaire.
Puis-je prendre contact avec vous uniquement pour avoir des informations générales ? Dois-je nécessairement passer chez vous, au siège de l’association ? Dois-je devenir membre ?
La revue MasciProûve est disponible gratuitement sur internet, elle peut déjà vous fournir certaines informations.
Vous pouvez prendre contact par courriel (voir mention légale), nous essayerons de vous répondre au mieux ou de vous rediriger vers des scientifiques d’Université selon vos besoins.
L’association possède un site « git » public des productions de codes rendues publiques.
Que me donne le statut de membre effectif ?
Si vous avez des questions plus précises (codage, manipulation) nous sommes disponibles. Vous pourrez échanger avec les autres membres. Vous aurez accès au « git » interne de l’association pour les développements en cours qui ne sont pas encore public. L’association achète des livres sur le sujet mais les membres peuvent aussi partager leur bibliothèque.
Que me donne le statut de membre adhérent ?
Vous pouvez consulter nos statuts pour plus d'informations: Moniteur belge
Ces services sont payants ?
Non ils sont contenus dans le montant d’adhésion annuel.
Êtes-vous prestataires de services B2B ?
Non, nous sommes des amateurs hobbyistes. Par contre, si vous êtes un professionnel (Entreprise,PME ou indépendant) du secteur ITP/ATP nous pouvons relayer, de façon neutre, vos propositions de services à des clients potentiellement intéressés qui prendraient contact avec nous.
Faut-il être geek ?
On ne se cache pas que le thème de l’association est assez « geek », pour ne pas dire complètement « geek ». Mais il n’est pas nécessaire d’être « geek » pour être membre. Nous accordons une importance également à l’aspect juridique, linguistique et éthique dans l’utilisation et le développement des ITP/ATP et de leur bibliothèque.
J’ai un avis critique contre les ITP/ATP, suis-je le bienvenu ?
Nous sommes ouverts à la critique des ITP/ATP. Si vous avez un avis argumenté, et même si vous n’êtes pas membre, il peut être publié dans la revue « MasciProûve » sous une rubrique « Avis externe ». Vous pouvez prendre contact avec l’association pour les modalités. L’organe d’administration se réserve le droit d’autoriser à la publication ou non.
Par contre, l’auto-destruction n’est pas un objectif de l’association : nous privilégions l’utilisation de l’outil information en personne prudente et raisonnable et non l’extinction de l’utilisation des ITP/ATP.
Comment puis-je devenir membre ?
Effectuer votre demande par courriel ou courrier postal (voir mention légale). Montant des cotisations (page 6, application art. 10 des status)
- Membre effectif: 40 EUR/an (non indexé)
  - 40,00 EUR/an au 1er janvier 2023
- Membre adhérent: 20 EUR/an (non indexé)
  - 20,00 EUR/an au 1er janvier 2023
- Tout membre peut demander, auprès de l’organe d’administration, une réduction de cotisation annuelle s’il justifie d’un statut d’étudiant, de chômeur, de prépensionné, de personne bénéficiant du revenu d’intégration du centre public d’aide sociale, de demandeur d’asile.
  La réduction de la cotisation annuelle des membres adhérents le demandant en application de l’aliéna 4 de l’article 10 du premier exercice social débutant le jour de la fondation et se terminant le 31 décembre 2022, en vertu de l’article 31 alinéa 2, est fixée à au moins la moitié de la cotisation d’un membre adhérent. Ainsi, le montant de la cotisation d’un membre adhérent demandant l’application de l’aliéna 4 de l’article 10 ne peut pas dépasser le montant de 10 EUR pour le premier exercice social. L'Assemblée générale a approuvé la prolongation de cette décision pour le second exercice social.
Faites-vous de la veille technologique ?
Comme la technologie évolue sans cesse, nous essayions, dans la mesure de nos moyens, de rester attentifs avec les dernières nouveautés.
Etes-vous des professionnels ?
Non, nous sommes tous des volontaires (voir. Rapport "Le volontariat dans l'union européenne").
Il n’y a pas de coordinateur/trice salarié(e).
Faites-vous des exposés dans les écoles, les salons d’éducation ?
Prenez toujours contact, on ne sait jamais que nous soyons disponibles.
L’association est constituée par des volontaires, nous ne vous garantissons pas que nous allons automatiquement rencontrer votre demande.
Attachez-vous de l'importance aux logiciels libres ?
Oui ! et non seulement aux logiciels libres mais aussi à la l'utilisation et à la production de bibliothèques libres !
Bref… à vous entendre on dirait un club d’astronomie mais pour logiciels particuliers...
Oui tout-à-fait !
Où puis-je trouver la revue « MasciProûve » ?
Une version numérique est disponible en téléchargement à l’adresse suivante MaSciProuve

Informations légales

"cafr-msa2p" asbl

Siège social:

Rue de la Brasserie, 5

7100 La Louvière Belgique

Num. Entreprise : 0777.779.751

RPM : Hainaut division Mons

IBAN : BE79 3632 1778 3733

Contact : Roland Coghetto, Organe d’Administration

roland.coghetto (a.r.o.b.a.s.e.)cafr-msa2p.be