.
Read the full article on GamingOnLinux.
.
Read the full article on GamingOnLinux.
.
Read the full article on GamingOnLinux.
.
Read the full article on GamingOnLinux.
.
Read the full article on GamingOnLinux.
.
Read the full article on GamingOnLinux.
En principe, une démonstration mathématique ne fait que suivre des règles logiques bien définies, et devrait donc pouvoir être encodée informatiquement et vérifiée par un ordinateur. Où en est-on dans la pratique et dans la théorie ? Petit tour au pays des assistants de preuve, des langages de programmation dédiés aux démonstrations, et de leur fondement théorique le plus commun, la théorie des types.
Comme nous sommes sur LinuxFr.org, je devrais peut-être commencer par ceci : tous, nous passons énormément de temps à découvrir des bugs, à les comprendre, à les résoudre, et de préférence à les éviter en écrivant des tests.
Dans une formation universitaire de base en informatique, on rencontre des algorithmes, mais aussi des méthodes pour prouver que ces algorithmes terminent et répondent bien au problème posé. Les premières introduites sont typiquement les variants de boucle (montrer qu’une certaine valeur décroît à chaque itération, ce qui assure que le programme termine si elle ne peut pas décroître à l’infini), et les invariants de boucle (montrer qu’une certaine propriété vraie au début d’une boucle est préservée entre deux itérations, ce qui assure qu’elle reste encore vraie à la fin de la boucle).
On a donc, d’une part, un algorithme, implémentable sur machine, d’autre part une preuve, sur papier, que l’algorithme est correct. Mais si l’implémentation a une erreur par rapport à l’algorithme sur papier ? Et puisque nous n’arrêtons pas de nous tromper dans nos programmes, il est fort possible que nous nous trompions dans notre preuve (qui n’a jamais oublié qu’il fallait faire quelque chose de spécial dans le cas ?).
En tant que programmeurs, on peut imaginer une approche où non seulement l’algorithme est implémenté, mais sa preuve de terminaison et de correction est aussi « implémentée », c’est-à-dire encodée dans un langage qui ressemble à un langage de programmation, pour être ensuite non pas interprétée ou compilée mais vérifiée.
La vérification est un très vaste domaine de l’informatique, dont je ne suis pas spécialiste du tout, et dans lequel il existe énormément d’approches : la logique de Hoare (voir par exemple l’outil why3), qui est essentiellement un raffinement des variants et invariants de boucle, la logique de séparation spécialement conçue pour raisonner sur la mémoire mutable (voir Iris), le model checking qui se concentre sur des programmes d’une forme particulièrement simple (typiquement des systèmes de transition finis) pour en vérifier des propriétés de façon complètement automatisée, etc.
Dans cette dépêche, je vais parler d’une approche avec quelques caractéristiques particulières :
On vérifie des programmes purement fonctionnels (pas d’effets de bord, même si on peut les simuler).
Le même langage mélange à la fois les programmes et leurs preuves.
Plus précisément, le langage ne fait pas (ou peu) de distinction entre les programmes et les preuves.
Pour se convaincre de l’ampleur que les démonstrations ont prise dans les mathématiques contemporaines, il suffit d’aller jeter un œil, par exemple, au projet Stacks : un livre de référence sur la géométrie algébrique, écrit collaborativement sur les 20 dernières années, dont l’intégrale totalise plus de 7500 pages très techniques. Ou bien la démonstration du théorème de classification des groupes finis simples : la combinaison de résultats répartis dans les dizaines de milliers de pages de centaines d’articles, et une preuve « simplifiée » toujours en train d’être écrite et qui devrait faire plus de 5000 pages. Ou bien le théorème de Robertson-Seymour, monument de la théorie des graphes aux nombreuses applications algorithmiques : 20 articles publiés sur 20 ans, 400 pages en tout. Ou bien, tout simplement, le nombre de références dans la bibliographie de la moindre thèse ou d’articles publiés récemment sur arXiv.
Inévitablement, beaucoup de ces démonstrations contiennent des erreurs. Parfois découvertes, parfois beaucoup plus tard. Un exemple assez célèbre est celui d’un théorème, qui aurait été très important s’il avait été vrai, publié en 1989 par Vladimir Voedvodsky, un célèbre mathématicien dont je vais être amené à reparler plus bas, avec Mikhail Kapranov. Comme raconté par Voedvodsky lui-même, un contre-exemple a été proposé par Carlos Simpson en 1998, mais jusqu’en 2013, Voedvodsky lui-même n’était pas sûr duquel était faux entre sa preuve et le contre-exemple !
Il y a aussi, souvent, des « trous », qui ne mettent pas tant en danger la démonstration mais restent gênants : par exemple, « il est clair que la méthode classique de compactification des espaces Lindelöf s’applique aussi aux espaces quasi-Lindelöf », quand l’auteur pense évident qu’un argument existant s’adapte au cas dont il a besoin mais que ce serait trop de travail de le rédiger entièrement. Donc, assez naturellement, un but possible de la formalisation des maths est de produire des démonstrations qui soient certifiées sans erreur (et sans trou).
Mais c’est loin d’être le seul argument. On peut espérer d’autres avantages, qui pour l’instant restent de la science-fiction, mais après tout ce n’est que le début : par exemple, on peut imaginer que des collaborations à grande échelle entre beaucoup de mathématiciens deviennent possibles, grâce au fait qu’il est beaucoup plus facile de réutiliser le travail partiel de quelqu’un d’autre s’il est formalisé que s’il est donné sous formes d’ébauches informelles pas complètement rédigées.
Parmi les assistants de preuve existants, la plupart (mais pas tous) se fondent sur une famille de systèmes logiques rangés dans la famille des « théories des types ». L’une des raisons pour lesquelles ces systèmes sont assez naturels pour être utilisés en pratique est qu’en théorie des types, les preuves et les programmes deviennent entièrement confondus ou presque, ce qui rend facile le mélange entre les deux.
Mais comment est-ce qu’un programme devient une preuve, au juste ? L’idée de base est appelée interprétation de Brouwer-Heyting-Kolomogorov et veut que les preuves mathématiques se comprennent de la façon suivante :
Le moyen de base pour prouver une proposition de la forme « et » est de fournir d’une part une preuve de et une preuve de . En d’autres mots, une preuve de « et » rassemble en un même objet une preuve de et une preuve de . Mais en termes informatiques, ceci signifie qu’une preuve de « et » est une paire d’une preuve de et d’une preuve de .
De même, pour prouver « ou », on peut prouver , ou on peut prouver . Informatiquement, une preuve de « ou » va être une union disjointe : une preuve de ou une preuve de , avec un bit pour savoir dans quel cas on est.
Pour prouver « Vrai », il suffit de dire « c’est vrai » : on a une unique preuve de « Vrai ».
On ne doit pas pouvoir prouver « Faux », donc une preuve de « Faux » n’existe pas.
Et le plus intéressant : pour prouver « si alors », on suppose temporairement et on en déduit . Informatiquement, ceci doit devenir une fonction qui prend une preuve de et renvoie une preuve de .
L’interprétation de Brouwer-Heyting-Kolmogorov est informelle, et il existe plusieurs manières de la rendre formelle. Par exemple, on peut interpréter tout ceci par des programmes dans un langage complètement non-typé, ce qui s’appelle la réalisabilité.
Mais en théorie des types, on prend plutôt un langage statiquement typé pour suivre l’idée suivante : si une preuve de et est une paire d’une preuve de et d’une preuve de , alors le type des paires de et peut se comprendre comme le type des preuves de « et ». On peut faire de même avec les autres types de preuves, et ceci s’appelle la correspondance de Curry-Howard. Autrement dit, là où Brouwer-Heyting-Kolmogorov est une correspondance entre les preuves et les programmes, Curry-Howard est un raffinement qui met aussi en correspondance les propositions logiques avec les types du langage, et la vérification des preuves se confond entièrement avec le type checking.
Sur les cas que j’ai donnés, la correspondance de Curry-Howard donne :
La proposition « et » est le type des paires d’un élément de et d’un élément de ,
La proposition « ou » est le type somme de et (comme Either en Haskell et OCaml, les tagged unions en C, et std::variant en C++ : l’un ou l’autre, avec un booléen pour savoir lequel),
La proposition « Vrai » est le type trivial à une seule valeur (comme () en Haskell et Rust, unit en OCaml),
La proposition « Faux » est le type vide qui n’a aucune valeur (comme ! en Rust),
La proposition « si alors » est le type des fonctions qui prennent un argument de type et renvoient une valeur de type .
La version de Curry-Howard que j’ai esquissée donne une logique dite « propositionnelle » : il n’y a que des propositions, avec des connecteurs entre elles. Mais en maths, on ne parle évidemment pas que des propositions. On parle de nombres, de structures algébriques, d’espaces topologiques, …, bref, d’objets mathématiques, et des propriétés de ces objets. Les deux types principaux de propositions qui manquent sont ce qu’on appelle les quantificateurs : « Pour tout , … » et « Il existe tel que… ». Ici, ce qui est une évidence en logique devient moins évident, mais très intéressant, du côté des programmes.
Prenons pour l’exemple le théorème des deux carrés de Fermat, qui énonce (dans l’une de ses variantes) qu’un nombre premier impair est de la forme si et seulement s’il peut s’écrire comme somme de deux carrés parfaits. À quoi doit ressembler le type associé à cette proposition ? Par analogie avec les implications, on a envie de dire que cela devrait être une fonction, qui prend un nombre premier impair , et renvoie une preuve de l’équivalence. Problème : ce qui est à droite de l’équivalence est une proposition paramétrée par . Autrement dit, en notant le type des nombres premiers impairs, on ne veut plus un simple type fonction , mais un type fonction où le type de retour peut dépendre de la valeur passée à la fonction, noté par exemple . Ces types qui dépendent de valeurs sont appelés types dépendants.
Dans les langages de programmation populaires, il est rare de trouver des types dépendants. Mais on en retrouve une forme faible en C avec les tableaux de longueur variable (VLA pour « variable-length arrays ») : on peut écrire
Connexion… f(int n) {
int array[n];
…
}
qui déclare un tableau dont la taille n est une expression. Néanmoins, en C, même si on dispose de ce type tableau qui est en quelque sorte dépendant, on ne peut pas écrire une fonction « int[n] f(int n) » qui renvoie un tableau dont la longueur est passée en paramètre. Plus récemment, en Rust, il existe les const generics, où des valeurs se retrouvent dans les types et où on peut écrire fn f<const n: usize>() -> [u8; n], ce qui est un vrai type dépendant, mais cette fois avec la restriction assez sévère que toutes ces valeurs peuvent être calculées entièrement à la compilation, ce qui à cause de la façon dont fonctionne ce type de calcul en Rust empêche par exemple les allocations mémoire. (Donc l’implémentation est assez différente, elle efface ces valeurs en « monomorphisant » tous les endroits où elles apparaissent.)
En théorie des types, le langage est (normalement) purement fonctionnel, donc les problèmes d’effets de bord dans les valeurs à l’intérieur des types dépendants ne se pose pas. Le type checking peut déclencher des calculs arbitrairement complexes pour calculer les valeurs qui se trouvent dans les types.
Et le « il existe », au fait, à quoi correspond-il ? Cette fois, ce n’est plus une fonction dépendante mais une paire dépendante : une preuve de « Il existe tel que » est une paire d’une valeur et d’une preuve de . La différence avec une paire normale est que le type du deuxième élément peut dépendre de la valeur du premier élément.
Comme on peut commencer à s’en douter, le fait d’avoir des types dépendants est utile pour prouver des affirmations mathématiques, mais aussi, bien qu’il puisse sembler inhabituel, pour prouver des programmes, et plus précisément pour encoder des propriétés des valeurs dans les types. Là où on aurait dans un langage moins expressif une fonction qui renvoie deux listes, avec une remarque dans la documentation qu’elles sont toujours de même taille, dans un langage avec des types dépendants, on peut renvoyer un triplet d’un entier , d’une liste dont le type indique qu’elle est de taille , et une deuxième liste elle aussi de taille . Et là où on aurait un deuxieme_liste[indice_venant_de_la_premiere] avec un commentaire que cela ne peut pas produire d’erreur, car les deux listes sont de même taille, on a un programme qui utilise la garantie que les deux listes sont de même taille, et le typage garantit statiquement que cette opération t[i] ne produira pas d’erreur.
Reprenons l’exemple du théorème des deux carrés de Fermat. Nous pouvons maintenant traduire cette proposition en un type : celui des fonctions qui prennent un nombre premier impair et renvoient une paire de :
Une fonction qui prend tel que et renvoie deux entiers accompagnés d’une preuve que ,
Réciproquement, une fonction qui prend et une preuve de , et renvoie tel que .
Prouver le théorème des deux carrés de Fermat en théorie des types, c’est donner un élément (on dit plutôt « habitant ») de ce type, soit un programme dont le langage peut vérifier qu’il a ce type. Mais que fait au juste ce programme quand on l’exécute ? On voit qu’il permet notamment de calculer une décomposition d’un nombre premier impair congru à 1 modulo 4 comme somme de deux carrés.
Là, c’est le côté « programmes » qui apporte un élément moins habituel du côté « preuves » : l’exécution d’un programme va correspondre à un processus de simplification des preuves. Notamment, si on a une preuve de « si alors » et une preuve de , on peut prendre la preuve de et remplacer chaque utilisation de l’hypothèse dans la preuve de « si alors », pour obtenir une preuve de qui peut contenir de multiples copies d’une même preuve de . Cette opération de simplification du côté logique correspond naturellement au fait que la manière en théorie des types de prouver à partir d’une preuve de et d’une preuve de est tout simplement d’écrire , et que calculer , informatiquement, se fait bien en remplaçant le paramètre de à tous les endroits où il apparaît par la valeur et à simplifier le résultat. On dit que la logique de Curry-Howard est constructive, parce qu’elle se prête à une interprétation algorithmique.
Mais ceci peut sembler gênant. Par exemple, il est trivial en maths « normales » de prouver que tout programme termine ou ne termine pas. Mais par Curry-Howard, une preuve que tout programme termine ou ne termine pas doit être une fonction qui prend un programme, et qui renvoie soit une preuve qu’il termine, soit une preuve qu’il ne termine pas. Autrement dit, si cette proposition censément triviale était prouvable dans Curry-Howard, on aurait un algorithme pour résoudre le problème de l’arrêt, ce qui est bien connu pour être impossible.
L’explication à cette différence tient au fait que la preuve « triviale » de cette proposition utilise une règle de déduction qui a un statut un peu à part en logique, dite règle du tiers exclu : pour n’importe quelle proposition , sans aucune hypothèse, on peut déduire « ou (non ) » (autrement dit, que est vraie ou fausse). Or cette règle n’admet pas d’interprétation évidente par Curry-Howard : le tiers exclu devrait prendre une proposition et renvoyer soit une preuve de , soit une preuve que est fausse (ce qui s’encode par « si alors Faux »), autrement dit, le tiers exclu devrait être un oracle omniscient capable de vous dire si une proposition arbitraire est vraie ou fausse, et ceci est bien évidemment impossible.
(Cela dit, si vous voulez vous faire mal à la tête, apprenez que c’est l’opérateur call/cc et pourquoi l’ajouter permet de prouver le tiers exclu. Exercice : call/cc existe dans de vrais langages, comme Scheme, pourtant on vient de voir que le tiers exclu semble nécessiter un oracle omniscient, comment expliquer cela ?)
Pour être précis, la logique sans le tiers exclu est dite intuitionniste (le terme constructive étant un peu flou, alors que celui-ci est précis). On peut faire des maths en restant entièrement en logique intuitionniste, et même si ce n’est pas le cas de l’écrasante majorité des maths, il existe tout de même un certain nombre de chercheurs qui le font, et ceci peut avoir divers intérêts. Il y a notamment l’interprétation algorithmique des théorèmes, mais aussi, de manière beaucoup plus avancée, le fait que certaines structures mathématiques (topos, ∞-topos et consorts) peuvent s’interpréter comme des sortes d’univers mathématiques alternatifs régis par les règles de la logique intuitionniste (techniquement, des « modèles » de cette logique), et que parfois il est plus simple de prouver un théorème en le traduisant à l’intérieur de l’univers et en prouvant cette version traduite de manière intuitionniste.
Pour pouvoir malgré tout raisonner en théorie des types de manière classique (par opposition à intuitionniste), il suffit de postuler le tiers exclu comme axiome. Du point de vue des programmes, cela revient à rajouter une constante qui est supposée avoir un certain type mais qui n’a pas de définition (cela peut donc rendre les programmes impossibles à exécuter, ce qui est normal pour le tiers exclu).
Si vous aviez décroché, c’est le moment de reprendre. Parlons un peu des assistants de preuve qui existent. Les plus connus sont :
Rocq, anciennement nommé Coq, développé à l’Inria depuis 1989, écrit en OCaml, sous licence LGPL 2.1. Il est assez lié à l’histoire de la théorie des types, car il a été créé par Thierry Coquand comme première implémentation du calcul des constructions, une théorie des types inventée par Coquand et devenue l’une des principales existantes. (Oui, Coq a été renommé en Rocq à cause de l’homophonie en anglais entre « Coq » et « cock ». J’apprécierais que les commentaires ne se transforment pas en flame war sur ce sujet très peu intéressant, merci.)
Lean, créé par Leonardo de Moura et développé depuis 2013 chez Microsoft Research, écrit en C++, placé sous licence Apache 2.0.
Agda, créé par Ulf Norrell en 1999, écrit en Haskell et sous licence BSD 1-clause.
D’autres que je connais moins, notamment Isabelle et F* (liste sur Wikipédia).
Pour illustrer comment peuvent fonctionner les choses en pratique, voici un exemple très simple de code en Agda :
open import Agda.Primitive using (Level)
open import Data.Product using (_×_; _,_)
swap : {ℓ₁ ℓ₂ : Level} → {P : Set ℓ₁} {Q : Set ℓ₂} → P × Q → Q × P
swap (p , q) = (q , p)Vue comme un programme, cette fonction swap inverse simplement les deux éléments d’une paire. Vue comme une preuve, elle montre que pour toutes propositions et , si et , alors et . Comme le veut Curry-Howard, les deux ne sont pas distingués. Les types et sont eux-mêmes dans des types avec un « niveau » , ceci parce que, pour des raisons logiques, il serait incohérent que le type des types soit de son propre type, donc on a un premier type de types , qui est lui-même de type , et ainsi de suite avec une hiérarchie infinie de niveaux appelés univers. À un niveau plus superficiel, on remarquera qu’Agda a une syntaxe qui ressemble fort à Haskell (et utilise intensivement Unicode).
Voilà la même chose en Rocq :
Definition swap {P Q : Prop} : P /\ Q -> Q /\ P :=
fun H => match H with conj p q => conj q p end.La syntaxe est assez différente et ressemble plutôt à OCaml (normal, vu que Rocq est écrit en OCaml et Agda en Haskell). Mais à un niveau plus profond, on voit apparaître un type Prop dont le nom évoque furieusement les propositions. Or j’avais promis que les propositions seraient confondues avec les types, donc pourquoi a-t-on un type spécial pour les propositions ?
En réalité, pour diverses raisons, il peut être intéressant de briser l’analogie d’origine de Curry-Howard et de séparer les propositions et les autres types en deux mondes qui se comportent de façon extrêmement similaire mais restent néanmoins distincts. Notamment, un principe qu’on applique sans réfléchir en maths est que si deux propositions sont équivalentes, alors elles sont égales (extensionnalité propositionnelle), mais on ne veut clairement pas ceci pour tous les types (on peut donner des fonctions bool -> int et int -> bool, pourtant on ne veut certainement pas bool = int), donc séparer les propositions des autres permet d’ajouter l’extensionnalité propositionnelle comme axiome. (Mais il y a aussi des différences comme l'imprédicativité dans lesquelles je ne vais pas rentrer.)
Et voici encore le même code, cette fois en Lean :
def swap {P Q : Prop} : P ∧ Q → Q ∧ P :=
fun ⟨p, q⟩ => ⟨q, p⟩À part les différences de syntaxe, c’est très similaire à Rocq, parce que Lean a aussi une séparation entre les propositions et les autres types.
Cependant, en Rocq et Lean, on peut aussi prouver la même proposition de façon différente :
Lemma swap {P Q : Prop} : P /\ Q -> Q /\ P.
Proof.
intros H. destruct H as [p q]. split.
- apply q.
- apply p.
Qed.et
def swap {P Q : Prop} : P ∧ Q → Q ∧ P := by
intro h
have p := h.left
have q := h.right
exact ⟨q, p⟩Avec Proof. ou by, on entre dans un mode où les preuves ne sont plus écrites à la main comme programmes, mais avec des tactiques, qui génèrent des programmes. Il existe toutes sortes de tactiques, pour appliquer des théorèmes existants, raisonner par récurrence, résoudre des inégalités, ou même effectuer de la recherche automatique de démonstration, ce qui s’avère extrêmement utile pour simplifier les preuves.
Ce mode « tactiques » permet aussi d’écrire la preuve de façon incrémentale, en faisant un point d’étape après chaque tactique pour voir ce qui est prouvé et ce qui reste à prouver. Voici par exemple ce qu’affiche Rocq après le destruct et avant le split :
P, Q : Prop
p : P
q : Q
============================
Q /\ P
Cette notation signifie que le contexte ambiant contient les variables P et Q de type Prop ainsi que p une preuve de P (donc un élément du type P) et q une preuve de Q. Le Q /\ P en dessous de la barre horizontale est le but à prouver, c’est-à-dire le type dont on cherche à construire un élément.
Agda fonctionne assez différemment : il n’y a pas de tactiques, mais il existe néanmoins un système de méta-programmation qui sert à faire de la recherche de preuves (donc contrairement à Rocq et Lean, on n’écrit pas la majeure partie des preuves avec des tactiques, mais on peut se servir d’un équivalent quand c’est utile). Pour écrire les preuves incrémentalement, on met ? dans le programme quand on veut ouvrir une sous-preuve, et Agda va faire le type-checking de tout le reste et donner le contexte à l’endroit du ?.
En 2025, la formalisation reste très fastidieuse, mais elle a déjà eu plusieurs grands succès :
Actuellement, Lean a réussi à attirer une communauté de mathématiciens qui développent mathlib (1,1 million de lignes de code Lean au moment où j’écris), une bibliothèque de définitions et théorèmes mathématiques qui vise à être la plus unifiée possible.
Les équivalents dans d’autres assistants de preuve se développent même s’ils ne sont pas (encore) aussi gros : citons mathcomp, unimath, agda-unimath entre autres.
Un autre grand succès, dans le domaine de la vérification cette fois, est CompCert (malheureusement non-libre), qui est un compilateur C entièrement écrit en Rocq et vérifié par rapport à une spécification du C également encodée en Rocq.
La théorie des types est un domaine de recherche à part entière, qui vise à étudier du point de vue logique les théories des types existantes, et à en développer de nouvelles pour des raisons à la fois théoriques et pratiques.
Historiquement, une grande question de la théorie des types est celle de comprendre à quel type doivent correspondre les propositions d’égalité. Par exemple, on veut que deux propositions équivalentes soient égales, et que deux fonctions qui prennent les mêmes valeurs soient égales, et éventuellement pour diverses raisons que deux preuves de la même proposition soient égales, mais s’il est facile d’ajouter toutes ces choses comme axiomes, il est très compliqué de les rendre prouvables sans obtenir, comme avec le tiers exclu, des programmes qui ne peuvent pas s’exécuter à cause des axiomes qui sont déclarés sans définition.
Vladimir Voedvodsky a fait une contribution majeure en proposant un nouvel axiome, appelé univalence, qui dit très sommairement que si deux types ont la même structure (on peut donner une « équivalence » entre les deux), alors ils sont en fait égaux (résumé simpliste à ne pas prendre au mot). Cet axiome est très pratique pour faire des maths parce qu’on travaille souvent avec des objets qui ont la même structure (on dit qu’ils sont isomorphes), et qui doivent donc avoir les mêmes propriétés, et cet axiome permet de les identifier (même s’il a aussi des conséquences qui peuvent paraître choquantes). Sa proposition a donné naissance à une branche appelée théorie homotopique des types, qui explore les maths avec univalence. Le prix à payer est que les types ne se comprennent plus comme de simples ensembles de valeurs (ou de preuves d’une proposition), mais comme des espaces géométriques munis de toute une structure complexe (techniquement, les égalités sont des chemins entre points, et il y a des égalités non-triviales, des égalités entre égalités, etc.), et la compréhension de ces espaces-types est fondée sur la théorie de l’homotopie. Il y a bien d’autres théories des types, avec univalence ou non : théorie cubique des types, théorie des types observationnelle, etc.
J’espère avoir communiqué un peu de mon enthousiasme pour le domaine (dans lequel je suis probablement parti pour démarrer une thèse). Si vous voulez apprendre un assistant de preuve, une ressource assez abordable est la série Software Foundations avec Rocq. Il existe également Theorem proving in Lean 4 et divers tutoriels Agda. Vous pouvez aussi essayer ces assistants de preuve directement dans votre navigateur : Rocq, Lean ou Agda. Et bien sûr les installer et jouer avec : Rocq, Lean, Agda.
Commentaires : voir le flux Atom ouvrir dans le navigateur
.
Read the full article on GamingOnLinux.
.
Read the full article on GamingOnLinux.
.
Read the full article on GamingOnLinux.
.
Read the full article on GamingOnLinux.
.
Read the full article on GamingOnLinux.
The 9to5Linux Weekly Roundup for February 23rd, 2025, brings news about Ubuntu 24.04.2 LTS, Mesa 25.0, KDE Plasma 6.3.1, PeaZip 10.3, Linux kernel 6.13 on Ubuntu, as well as all the latest distro and software updates.
The post 9to5Linux Weekly Roundup: February 23rd, 2025 appeared first on 9to5Linux - do not reproduce this article without permission. This RSS feed is intended for readers, not scrapers.
.
Read the full article on GamingOnLinux.
A set of four cool new window opening and closing animations got added to gaudy GNOME Shell extension Burn My Windows this weekend. A veritable Linux eye-candy essential, Burn My Windows makes it easy to apply a variety of visual effects to Ubuntu when opening and/or closing app windows, dialogs, and modals. Its sole purpose is to make using Linux a bit more entertaining. Burn My Windows v45 is the latest update. It adds support for the upcoming GNOME 48 release (which will ship in Ubuntu 25.04 this April), fine-tunes effect filtering in Preferences, and improves its Incinerate effect with […]
You're reading 4 New Effects Added to ‘Burn My Windows’ GNOME Extension, a blog post from OMG! Ubuntu. Do not reproduce elsewhere without permission.
Calendrier Web, regroupant des événements liés au Libre (logiciel, salon, atelier, install party, conférence), annoncés par leurs organisateurs. Voici un récapitulatif de la semaine à venir. Le détail de chacun de ces 37 événements (France: 34, internet: 3) est en seconde partie de dépêche.
Montpel'libre réalise une série d’émissions régulières à la Radio FM-Plus intitulées « Temps Libre ». Ces émissions sont la présentation hebdomadaire des activités de Montpel’libre.
Après le jingle où l’on présente brièvement Montpel'libre, nous donnerons un coup de projecteur sur les activités qui seront proposées prochainement.
Ces émissions seront l’occasion pour les auditeurs de découvrir plus en détails les logiciels libres et de se tenir informés des dernières actualités sur le sujet.
Alors, que vous soyez débutant ou expert en informatique, que vous ayez des connaissances avancées du logiciel libre ou que vous souhaitiez simplement en savoir plus, Montpel'libre, au travers de cette émission, se fera un plaisir pour répondre à vos attentes et vous accompagner dans votre découverte des logiciels libres, de la culture libre et des communs numériques.
Vous vous demandez peut-être ce qu’est un logiciel libre. Il s’agit simplement d’un logiciel dont l’utilisation, la modification et la diffusion sont autorisées par une licence qui garantit les libertés fondamentales des utilisateurs. Ces libertés incluent la possibilité d’exécuter, d’étudier, de copier, d’améliorer et de redistribuer le logiciel selon vos besoins.
Inscription | GPS 43.60524/3.87336
Fiche activité:
https://montpellibre.fr/fiches_activites/Fiche_A5_017_Emission_Radio_Montpellibre_2024.pdf
Vous voulez vous engager pour une cause, rencontrer de nouvelles personnes et découvrir la cartographie participative et humanitaire? CartONG vous invite à participer à un ou plusieurs mapathons en ligne! 🗺️💻
Venez cartographier les régions encore absentes des cartes pour soutenir les organisations humanitaires et de solidarité internationale qui ont besoin de cartes précises et à jour pour agir plus efficacement en cas de crise ou initier des projets de développement local.
Les ateliers de cartographie sont organisés dans le cadre du projet Missing Maps, qui a pour objectif de cartographier de façon préventive les régions vulnérables aux catastrophes naturelles, crises sanitaires, environnementales, aux conflits et à la pauvreté. On peut penser qu’aujourd’hui toutes les parties du monde sont cartographiées, mais en réalité de nombreuses régions ne possèdent encore aucune carte!
🤔 Pour qui? Pas besoin d’être un·e expert·e, les ateliers sont accessibles à tout le monde!
📌 Où ? 100% en ligne! Un lien de connexion vous sera envoyé après votre inscription
🖱️ Comment? Avec la plateforme de cartographie libre et contributive OpenStreetMap (OSM, le «Wikipédia des cartes») tout le monde peut participer à la cartographie de n’importe quelle zone de la planète: il suffit d’un ordinateur, d’une souris et d’une connexion internet! Accessibles à tout·es, nous serons là pour vous accompagner pour vos premiers pas avec OSM.
Le programme des mapathons
18h00: Introduction, présentation de la cartographie collaborative et solidaire et démonstration OSM pour les nouveaux·elles
18h30: On cartographie tous ensemble sur un projet
20h00: Fin du mapathon, conclusion sur les contributions de la soirée
Pour s’inscrire c’est par ici
Si vous avez besoin de plus d’info, vous pouvez nous contacter directement à l’adresse suivante: missingmaps@cartong.org
Depuis la rentrée 2023, les temps de rencontre autour d’OpenStreetMap sont relancés.
L’occasion de se rencontrer (ou de se retrouver), d’échanger sur OpenStreetMap et de lancer des projets en commun.
L’émission Libre à vous! de l’April est diffusée chaque mardi de 15 h 30 à 17 h sur radio Cause Commune sur la bande FM en région parisienne (93.1) et sur le site web de la radio.
Le podcast de l’émission, les podcasts par sujets traités et les références citées sont disponibles dès que possible sur le site consacré à l’émission, quelques jours après l’émission en général.
Les ambitions de l’émission Libre à vous!
Découvrez les enjeux et l’actualité du logiciel libre, des musiques sous licences libres, et prenez le contrôle de vos libertés informatiques.
Donner à chacun et chacune, de manière simple et accessible, les clefs pour comprendre les enjeux mais aussi proposer des moyens d’action, tels sont les objectifs de cette émission hebdomadaire.
L’émission dispose:
Radio Cause Commune,
Rencontres Accès Libre
Certains les appellent «install party», d’autres encore «Soirées Linux», mais les Rencontres Accès Libre sont tout cela en même temps, et bien plus encore…
Entre autres, c’est l’occasion de:
C’est un évènement organisé conjointement par Linux Azur et le SHL.
L’association PauLLA organise son assemblée générale annuelle le mardi 25 février 2025 à Pau.
Si vous voulez découvrir l’association, rencontrer ses membres et échanger avec le bureau, c’est le meilleur moment de l’année. Rejoignez-nous pour promouvoir le logiciel libre à Pau et dans les environs.
Toutes les infos sont sur cette page: https://www.paulla.asso.fr/Evenements/assemblee-generale-paulla-2025
Au plaisir de vous rencontrer !
Vous avez décidé de reprendre en main votre vie numérique? Venez nous rencontrer le dernier mardi de chaque mois au Café Citoyen à Lille!
La permanence associative autour du Libre est une manifestation conviviale, ouverte à toutes et tous, organisée le dernier mardi (ou jeudi) de chaque mois par les collectifs de Chtinux (Raoull, Deuxfleurs, Mycélium, CLX, Cliss XXI…).
Rejoignez-nous pour y discuter joyeusement de Logiciel Libre, de Culture Libre, de données ouvertes (open data), de bidouille sous Linux, ou proposer vos idées d’évènements.
C’est aussi l’occasion d’obtenir un coup de main si vous rencontrez une difficulté sous Linux, ou si vous avez besoin de conseils pour migrer sur du Logiciel Libre.
Si vous venez avec votre ordinateur pour obtenir de l’aide technique, pour permettre à l’équipe bénévole de s’organiser, prévenez-nous via un courrier électronique à l’adresse: chtinux-diffusion CHEZ deuxfleurs POINT fr.
Le Café Citoyen est accessible en métro (station République – Beaux Arts). Une connexion Internet y est disponible, des prises électriques, de la place… Au bar, vous trouverez aussi de bonnes boissons avec et sans alcool, ainsi que de la petite restauration (notamment fromage ou tartines véganes).
Pour soutenir le Café Citoyen, nous vous demandons d’y acheter au minimum une consommation. Après avoir pris votre boisson ou votre en-cas au bar, vous pouvez nous rejoindre directement au deuxième étage.
Au plaisir de vous retrouver!
L’association Ailes-52 tient sa permanence numérique tous les mardis à 20h.
Pour les adhérents ou visiteurs curieux, qui souhaitent:
Alors venez nous rencontrer et discuter lors de cette permanence.
rendez-vous est donné aux participants à 20h à l’adresse: https://visio.chapril.org/ailes52-permanence-web
Un temps d’accueil et de présentation sera consacré aux participants, à l’identification des thématiques que chacun souhaite aborder, au temps à y consacrer et aux éventuels groupes de travail à constituer
~ 20h30 à 21h30: séance de travail sur les thématiques identifiées avec échanges sur la fin d’atelier
La séance de travail se terminera au maximum à 21h30, le salon restera disponible pour des échanges éventuels entre les participants sans les animateurs.
Ailes-52 est une association loi 1901 reconnue d’intérêt général.
L’atelier est animé par des bénévoles de l’association.
Assistance technique et démonstration concernant les logiciels libres.
Il est préférable de réserver votre place à contact (at) linuxmaine (point) org
Planning des réservations consultableici.
Échanger sur Linux et les Logiciels Libres,
Acheter un ordinateur reconditionné,
Gérer mes contacts sur mon ordiphone et mon PC,
Installer/configurer un logiciel libre sous Linux,
Configurer une imprimante/scanner,
Essayer une distribution Linux,
Installer GNU/Linux sur mon ordi c’est possible ?
Cours d’espéranto tous les mercredis de 17h30 à 19h,
Université Bordeaux Montaigne,
Esplanade des Antilles,
Domaine Universitaire
33600 Pessac
Les cours sont animés par Elvezio & Jean-Seb. Ils sont totalement gratuits et sans droits d’inscription à la fac, 100% gratuits.
Veuillez contacter le 06 72 17 22 97 avant votre venue afin de connaître la salle ou pour plus d’informations.
Le groupe local Nancy de l’association OpenStreetMap France vous propose de participer aux réunions mensuelles ouvertes à tou·te·s !
Avec OpenStreetMap, participez à la construction d’une carte en ligne libre et gratuite, partagée avec le monde entier!
Participation aux ateliers
Le lieu la Fabrique des possibles nous est librement accessible lors de nos réunions.
Si vous souhaitez participer à distance, cela est possible depuis ce lien. Toutefois merci de nous en avertir pour que nous nous organisions en nous équipant et installant le matériel nécessaire.
Chaque mercredi soir, l’association propose une rencontre pour partager des connaissances, des savoir-faire, des questions autour de l’utilisation des logiciels libres, que ce soit à propos du système d’exploitation Linux, des applications libres ou des services en ligne libres.
C’est l’occasion aussi de mettre en avant l’action des associations fédératrices telles que l’April ou Framasoft, dont nous sommes adhérents et dont nous soutenons les initiatives avec grande reconnaissance.
Nous poursuivons ces rencontres et vous proposons d’échanger
autour de nos outils numériques quotidiens et des alternatives possibles.
Participez au prochain Ĝblabla à Parempuyre (33)
🥁 Dans le (joli) cadre des rencontres mensuelles du ĞBlabla en Gironde, donnons-nous cette fois rendez-vous à Parempuyre (33), le 26 février 2025 à partir de 18:30 et jusqu’à 22:00/22:30, pour des questions/réponses sur la Monnaie Libre Ğ1 et sur la Monnaie Locale la Gemme, pour des découvertes de Cesium, des certifications… et bien sûr, pour manger et boire ce que nous apporterons !
L’adresse exacte vous sera donnée lors de votre inscription – alors vous savez ce qu’il vous reste à faire 😀 À bientôt !
Rézine est un fournisseur d’accès à Internet qui défend une vision politique des technologies et des réseaux. Pour cela, Rézine met notamment en œuvre un accès Internet local, à prix juste, respectant la neutralité du Net, piloté par ses usagères et usagers, dans une démarche émancipatrice.
Nous fournissons Internet via la fibre, via wifi (radio) et proposons également des VPN.
Par ailleurs, fournir une critique du numérique, et en particulier des réseaux, est une activité inhérente à notre activité de fournisseur d’accès à Internet, que nous avons affirmée dans l’objet de la structure. Nous inscrivons notre démarche dans une tradition d’éducation populaire, qui vise à contribuer à l’émancipation des personnes, dans leur rapport aux technologies et aux réseaux, quel que soit leur niveau de connaissance.
Venez nous rencontrer pour discuter, devenir membre, poser vos questions sur la fibre, sur Internet, ou juste par curiosité!
Ces rencontres mensuelles se veulent être des instants conviviaux pour faire un compte-rendu des activités du mois précédent, mais aussi pour présenter les opérations et rendez-vous à venir que proposent les groupes HérOSM. Naturellement, elles sont également ouvertes à tout public, en présence et à distance.
Si vous avez des propositions n’hésitez pas à compléter la page dédiée.
Programme:
Déroulement de la rencontre
Nous vous présenterons les projets en cours, nous vous proposerons de contribuer, faire de la production de données.
Comme d’habitude, chacun amène ce qu’il veut à manger et à boire pour un repas partagé.
N’oubliez pas vos ordinateurs portables pour la séance de saisie!
Tramway lignes 1 et 3, arrêts Port-Marianne et Rives du Lez
GPS Latitude: 43.603095 | Longitude: 3.898166
Carte OpenStreetMap
Programmation des Ateliers du Libre 2025
De janvier à mai 2025, Résoudre vous propose 6 ateliers numériques de 3 séances pour découvrir les logiciels libres (gratuits).
TRAITEMENT DE TEXTE
TABLEAU DE CALCUL
DIAPORAMA
TRAITEMENT VIDEO
RETOUCHE PHOTO
MIXAGE AUDIO
OUVERT TOUT PUBLIC, Inscrivez-vous à l’accueil.
Participation sous forme d’adhésion 10 € par atelier de 3 séances.
Télécharger ici la programmation «Ateliers du Libre 2025»
Dans le cadre des JPO, La Palanquée en fête.
Venez découvrir Linux et vous faire aider pour l’installer et à la prise en main, dans différents lieux, dans et à proximité de la métropole montpelliéraine
L’équipe de Montpel’libre vous propose une permanence Logiciels Libres : discussions libres et accompagnements techniques aux systèmes d’exploitation libres pour vous aider à vous familiariser avec votre système GNU/Linux au quotidien.
Le contenu de l’atelier s’adapte aux problèmes et aux questionnements des personnes présentes avec leur(s) ordinateur(s), qu’il soit fixe ou portable, et permet ainsi l’acquisition de nouvelles compétences nécessaires à une autonomie numérique certaine, au rythme de chacun.
Les thèmes :
Vous pourrez y aborder plusieurs thèmes (liste non exhaustive) :
Les permanences techniques ont lieu une fois par semaine, dans un lieu et à des jours et heures différents.
Entrée libre et gratuite sur inscription. Une simple adhésion à l’association est possible. Rejoindre le groupe Montpel’libre sur Telegram S’inscrire à la Newsletter de Montpel’libre.
Sur inscription | GPS 43.405195/3.695778
Fiche activité: https://montpellibre.fr/fiches_activites/Fiche_A5_002_Permanence_GNU-Linux_Montpellibre_2024.pdf
Le groupe d’utilisateurs de logiciels libres de Toulouse Toulibre en collaboration avec Tetaneutral.net fournisseur d’accès internet et hébergeur libre proposent aux sympathisants de se retrouver l’un des mardis ou jeudis de chaque mois pour échanger autour des logiciels libres, des réseaux libres, discuter de nos projets respectifs et lancer des initiatives locales autour du Libre. Ce repas est ouvert à tous, amateurs de l’esprit du Libre, débutants ou techniciens chevronnés.
Ce Qjelt aura lieu le jeudi 27 février 2025 à 20h30, au restaurant la Paniolade situé au 146 Boulevard de Suisse à Toulouse. C’est à proximité des ponts jumeaux et des minimes, et donc accessible par bus ou métro même tard le soir (bus 16 ou métro B en marchant un peu). Il n’y a pas de formule prévue, c’est à la carte : pizzas, viandes, poissons, salades…
Pour des raisons de logistique, une inscription préalable avant la veille est demandée sur toulibre.org/qjelt
Médiathèque de Quimperlé, place Saint Michel, pas d’inscription, entrée libre !
Mickaël, Johann, Alain, Pierre, et Yves vous accueillent (ou l’un d’eux, on se relaie !).
Conseils, aide et infos pratiques GNU/Linux et Logiciels Libres.
Curieux ? Déjà utilisateur ? Expert ? Pour résoudre vos problèmes, vous êtes le bienvenu ; pas besoin de prendre rendez-vous !
N’hésitez pas à venir avec votre PC si vous voulez une installation de GNU/Linux ou de venir avec votre périphérique récalcitrant (imprimante, scanner…) si possible.
On vous accueille tous les premiers mercredi du mois de 16h à 18h30 à la Maison de l’Économie Circulaire : 36 cours général giraud 69001 Lyon (Maison qui se situe dans le parc des Chartreux)
Conseil et aide à la réparation:
On vous accompagne dans l’entretien, la réparation ou le reconditionnement de votre ordinateur Vente d’ordinateurs à prix solidaires:
Ordinateurs fixes et portables à petit prix reconditionnés par nos soins sous Linux Reconditionnement solidaire:
Vous aimez bidouiller des ordis ? Venez nous filer un coup main ! Ouvert à tous et à toutes sans inscription
Pour toutes questions: contact@eisenia.org
Dans le cadre de son animation "Répar'Café", l'Alternativ', Tiers Lieu Numérique
Propose une présentation du système informatique gratuit et sécurisé,
capable de régénérer un vieil ordinateur.
Pour installer des logiciels libres sur sa machine personnelle en se faisant conseiller
et aider par des membres du groupe d’utilisateurs.
Pour tous: grands débutants et curieux, connaisseurs et experts sont bienvenus !
Ordinateurs à disposition pour découvrir.
L’AGU3L Logiciels Libres à Annecy votre association se réunit tous les vendredis à partir 20h00 et jusque vers 1h00 du matin. Passez quand vous voulez.
Entrée par le côté, entre les 2 bâtiments la MJC le Cairn et la maison des associations. La salle est au fond du couloir à droite, là où il y a de la lumière.
⚠️ Vérifiez sur le site avant de vous déplacer, y a un bandeau en haut qui confirme bonne la tenue de la réunion.
Le programme de la réunion, s’il y en a un, est sur notre site. 😉 ⬇️
Ou sur Mastodon https://piaille.fr/@agu3l
Digression du programme possible, voire probable.
Vous pouvez aussi nous soumettre un ou plusieurs sujets de programme:
Exemples:
Libre Office les listes à puces, j’aimerais en savoir plus
Pouvez-vous nous présenter le système Linux pour les débutants ?
plus technique: recompiler un noyau Linux avec les options spécifiques
Kubernetes est-ce pour moi ?
Démo sur un logiciel libre en particulier ex: Gimp, flameshot
Ou même votre logiciel que vous souhaitez partager
À l’aide ! 😱 pas de panique, on a probablement une solution pour vous.
Vous développez du code libre ? oui
etc, etc.
Apportez à boire, à manger. Un ordi ça peut aider. De la bonne humeur et un brin de Liberté.
Et tout ce que vous trouvez sympa: des amis, des projets, des trouvailles, etc.
Besoin d’une installation Linux?
Pas de problème! Laissez-nous un petit message avant au cas où l’on soit pas dispo ce soir-là.
C’est install party à la demande !
Utilisation d’internet sans flicage et efficacement
DNS, adresse internet, continuer sans accepter, sécurisé, flicage, fake news, réseaux sociaux, adresse IP, chercher une recette de soupe à l’oignon, d’aïoli ou de Jalebi facile.
Être sur internet sans maitriser quelques notions de base c’est faire du vélo sans chaine sur l’autoroute.
Pour mettre tout ça au clair, tous les Samedis du 18 janvier 2025 au 8 mars 2025, de 9h à 12h, Micro Môle organise des ateliers pour tout âge et tout niveaux.
Il est conseillé de suivre dans l’ordre chacun des ateliers, mais vous pouvez venir en cours de saison.
Ouvert à tous les niveaux, dès 14 ans jusqu’à 110 ans.
Laquadrature du net, vous connaissez?
Animé par le 'collectif les fous du code'.
Le rendez-vous mensuel pour partager nos connaissances et échanger nos savoirs du monde du numérique.
Le 1ᵉʳ Samedi dès 9h00 à 12h00
Le premier samedi de chaque mois (sauf août et septembre), de 9h30 à 18h, nous organisons une journée porte ouverte pour présenter notre association et son but.
Lors de cette journée vous êtes invités à venir nous rencontrer pour découvrir les possibilités des logiciels libres.
Venez avec vos questions, vos souhaits, vos matériels, nous verrons ensemble comment y répondre.
Nous acceptons le don de Matériels informatique (surtout portables), Tablette et Smartphone, de préférence avec leur alimentation / chargeur.
Le Wiki pour vous aider à passer au Libre: https://wiki.llv.asso.fr/doku.php
Pour le déjeuner, une participation vous sera demandé.
IMPORTANT: Lisez la "Préparation pour l’installation": https://wiki.llv.asso.fr/doku.php?id=wiki:installer:preparation_installation
Localisation précise: https://www.openstreetmap.org/note/4365747
Proche du Métro (13) Malakoff Plateau de Vanves (à 5 minutes)
Cet atelier convivial d’auto-réparation et d’entretien des appareils électriques, électroniques et informatiques a pour objectif de les faire durer, réduire les déchets et nous rendre plus autonomes face aux technologies.
Tu n’oses pas ouvrir ton grille-pain ou ton mixer en panne ? Ton écran de smartphone est cassé ? Ton ordinateur devient très très lent ?
À l’aide de multimètre, tournevis et d’outils informatiques libres, on s’entraide et on trouve la solution ensemble.
Cet atelier est gratuit et ouvert à tous, que tu sois un bricoleur qui souhaite aider ou que tu aies besoin d’être aidé.
Attention, tous les intervenants sont bénévoles et il n’y a aucune garantie de succès, mais nous pourrons t’orienter vers des professionnels en cas de besoin.
En attendant ce rendez-vous, tu peux consulter les fiches informatiques de l’atelier numérique des 3L: ricochets-figeac.fr
Tous les premiers samedis du mois et le vendredi après-midi qui suit.
Présentation de l’E2L
Quel est le rôle de l’école du logiciel libre?
Tout d’abord, ce n’est pas une école comme les autres. Elle n’a pas d’établissement fixe, pas de cours de récréation, pas de carte d’étudiant, ni de diplôme de fin d’année.
Comme toutes les écoles, son rôle est d’apprendre à ses élèves les logiciels libres, c’est-à-dire:
En fait, l’école du logiciel libre est une université populaire, comme celles qui ont vu le jour en France à partir du 19ᵉ siècle, et dont le but est de transmettre des connaissances théoriques ou pratiques à tous ceux qui le souhaitent. Et pour atteindre ce but, sa forme juridique est de type « association à but non lucratif ».
Comment fonctionne l’école?
Cette école étant une association, elle possède, comme toutes les autres, un bureau, élu chaque année en assemblée générale, pour l’administrer. Mais elle a aussi des responsables pédagogiques dont le rôle est essentiel, car ce sont eux qui établissent les programmes des cours en fonction des souhaits des adhérents, valident les candidatures des enseignants et affectent les sessions.
Les membres du bureau et les responsables pédagogiques forment « l’encadrement de l’école ». Tous les membres “encadrants” doivent être membres de l’association.
Les locaux où se déroulent les cours seront ceux que l’on veut bien nous prêter: une salle des fêtes, un théâtre, une salle de réunion publique, un amphi dans une école publique, ou autre.
Les thèmes des cours sont définis par les adhérents en fonction de leurs envies, de leurs besoins. Les cours sont ensuite décidés par les responsables pédagogiques de l’école en fonction des enseignants disponibles.
Afin de permettre au plus grand nombre de participer et d’assister aux cours, les sessions se tiennent essentiellement le samedi. Une première, sous forme d’atelier public, de 10h30 à 13h, et une autre, sous forme de cours, de 14h30 à 18h30.
Programme détaillé sur le site http://e2li.org
Créer sa BD interactive en 7 étapes. Session 5.
Rassemblez le scénario, les assets et l’interface pour préparer votre BD.
Créer sa BD interactive en 7 étapes. Session 6.
Découvrez le Sound Design.
Assistance technique et démonstration concernant les logiciels libres.
Attention, réservez votre place par contact (at) linuxmaine.org
Planning des réservations consultableici.
Tous les samedis de 16h à 18h, Linux Quimper vous donne rendez-vous au centre social des Abeilles, 4 rue Sergent Le Flao (quartier de la Terre Noire) Quimper.
Nous vous proposons lors de ces rencontres d’échanger autour du Libre et de Linux en particulier
Vous pouvez venir pour vous faire aider, ou aider, à installer et paramétrer une distribution GNU/Linux de votre choix ou des logiciels libres sur votre ordinateur.
Recommandations:
Vous pouvez aussi venir pour une première prise d’informations et de contacts.
Samedi 1ᵉʳ mars #AtelierLibre #Cartographie Participative, entre 17h et 19h à la Maison du temps libre de Saint Martin de Tallevende, #Vire #Normandie.
L’objectif est de se familiariser avec la cartographie participative et d’apporter sa contribution sur un projet concret sur Vire, avec #JOSM, un éditeur de données d’OpenStreetMap.
Cet atelier permettra d’apprendre à contribuer individuellement pour corriger facilement des manques ou compléter des informations sur #OpenStreetMap.
Samedi 1ᵉʳ mars 2025 | à 19h | Médiathèque du CanalQuai François Truffaut, 78180 Montigny-le-Bretonneux
Plongez dans l’univers fascinant des hackers à travers des extraits cultes de films et séries ! Véritables génies de l’ombre ou légendes amplifiées par Hollywood ? Entre réalités techniques et fantasmes cinématographiques, nos experts décrypteront avec vous les mythes et enjeux de la cybersécurité.
Démos, quiz, débats, popcorn et convivialité pour une soirée immersive !
Que vous soyez passionné d’informatique, curieux ou cinéphile, cette soirée unique est faite pour vous. Venez échanger et explorer ce monde mystérieux dans une ambiance décontractée.
Entrée libre – Venez avec vos questions et votre curiosité !
Lien médiathèque :
https://e-mediatheque.sqy.fr/Default/doc/CALENDAR/7478/soiree-cult-au-canal
pour venir:
RER C
Lignes N et U
Pour en savoir plus:
https://root66.net/?post/2025/02/20/Soir%C3%A9e-Cult%E2%80%99-plong%C3%A9e-dans-l%E2%80%99univers-du-hacking-%3A-Dans-l%E2%80%99%C5%93il-des-experts
Repair café, atelier informatique, etc.
Tous les premiers dimanches du mois à “Mosaïque”.
Commentaires : voir le flux Atom ouvrir dans le navigateur
Deux-cent trente-cinquième émission « Libre à vous ! » de l’April. Podcast et programme :
Rendez‐vous en direct chaque mardi de 15 h 30 à 17 h sur 93,1 FM en Île‐de‐France. L’émission est diffusée simultanément sur le site Web de la radio Cause Commune.
Mardi 25 février 2025, notre sujet principal portera sur le réseau français des FabLabs. Si vous avez des questions, n’hésitez pas à les mettre en commentaires de cette dépêche.
Commentaires : voir le flux Atom ouvrir dans le navigateur
PeaZip 10.3 open-source and free archive manager is now available for download with better integration with the GNOME and KDE Plasma desktops, a new Linux theme, and other changes. Here's what's new!
The post PeaZip 10.3 Archive Manager Improves Integration with GNOME and KDE Plasma appeared first on 9to5Linux - do not reproduce this article without permission. This RSS feed is intended for readers, not scrapers.
