Julien Narboux
@jnarboux.bsky.social
Researcher in Computer Science, IRIF, Université Paris Cité.
Topics of interest: proof assistants, ITP, ATP, teaching with proof assistants.
Topics of interest: proof assistants, ITP, ATP, teaching with proof assistants.
Oui je suis assez d'accord avec vous, la puissance de AlphaGeometry reside surtout à mon sens dans une généralisation de la méthode "Deductive Database" avec un pivot de Gauss pour automatiser certains calculs. Pas clair que le LLM ne puisse pas être remplacé par une heuristique.
August 28, 2025 at 12:25 PM
Oui je suis assez d'accord avec vous, la puissance de AlphaGeometry reside surtout à mon sens dans une généralisation de la méthode "Deductive Database" avec un pivot de Gauss pour automatiser certains calculs. Pas clair que le LLM ne puisse pas être remplacé par une heuristique.
Quand il y a des problèmes d'orientation (inégalités), alors il faut la CAD et la complexité théorique et en pratique ne permet pas de résoudre des problèmes avec beaucoup de points.
August 28, 2025 at 12:22 PM
Quand il y a des problèmes d'orientation (inégalités), alors il faut la CAD et la complexité théorique et en pratique ne permet pas de résoudre des problèmes avec beaucoup de points.
Oui les méthodes algébrique (Wu ou Gröbner) ou semi-algébrique (Méthode de aires) sont très efficaces pour les problèmes qui sont dans leur scope. Mais ces méthodes ne génèrent pas de preuve lisibles.
August 28, 2025 at 12:20 PM
Oui les méthodes algébrique (Wu ou Gröbner) ou semi-algébrique (Méthode de aires) sont très efficaces pour les problèmes qui sont dans leur scope. Mais ces méthodes ne génèrent pas de preuve lisibles.
Une petite pensée pour ses proches .
August 3, 2025 at 7:03 AM
Une petite pensée pour ses proches .
Et si tu veux t'en servir avec tes étudiants y a des interfaces comme Lean Verbose, Coq Waterproof et Yalep: gricad-gitlab.univ-grenoble-alpes.fr/yalep/Yalep
Yalep / Yalep · GitLab
Yalep is a micro language based on Lean for teaching mathematical high-school proofs
gricad-gitlab.univ-grenoble-alpes.fr
July 4, 2025 at 11:59 AM
Et si tu veux t'en servir avec tes étudiants y a des interfaces comme Lean Verbose, Coq Waterproof et Yalep: gricad-gitlab.univ-grenoble-alpes.fr/yalep/Yalep
Reposted by Julien Narboux
Quel beau dossier dans le nouveau numéro de La Recherche!
A titre personnel, j'ai commencé par l'article de Antoine Chambert-Loir sur les assistants de preuve et l'entretien avec Bernadette Bensaude-Vincent et Gabriel Dorthe sur la neutralité scientifique mais il y en a pour tous les goûts!
A titre personnel, j'ai commencé par l'article de Antoine Chambert-Loir sur les assistants de preuve et l'entretien avec Bernadette Bensaude-Vincent et Gabriel Dorthe sur la neutralité scientifique mais il y en a pour tous les goûts!
June 19, 2025 at 9:07 AM
Quel beau dossier dans le nouveau numéro de La Recherche!
A titre personnel, j'ai commencé par l'article de Antoine Chambert-Loir sur les assistants de preuve et l'entretien avec Bernadette Bensaude-Vincent et Gabriel Dorthe sur la neutralité scientifique mais il y en a pour tous les goûts!
A titre personnel, j'ai commencé par l'article de Antoine Chambert-Loir sur les assistants de preuve et l'entretien avec Bernadette Bensaude-Vincent et Gabriel Dorthe sur la neutralité scientifique mais il y en a pour tous les goûts!
Last week, our 15yo internship students proved that √2 is not rational using Frederic Tran Minh's "Yalep" (a layer above Lean) gricad-gitlab.univ-grenoble-alpes.fr/yalep/Yalep
Yalep / Yalep · GitLab
Yalep is a micro language based on Lean for teaching mathematical high-school proofs
gricad-gitlab.univ-grenoble-alpes.fr
June 27, 2025 at 2:44 PM
Last week, our 15yo internship students proved that √2 is not rational using Frederic Tran Minh's "Yalep" (a layer above Lean) gricad-gitlab.univ-grenoble-alpes.fr/yalep/Yalep
Signez la pétition pour le palais de la découverte ! chng.it/jdzbRhp5Qm
Signez la pétition
Sauvons le Palais de la découverte
chng.it
June 17, 2025 at 11:33 AM
Signez la pétition pour le palais de la découverte ! chng.it/jdzbRhp5Qm
Reposted by Julien Narboux
[ #VeilleESR #LRU ] Rapport Hcéres sur l'IHU Méditerranée.
« Ces recommandations sont impératives et devraient être satisfaites avant toute décision de refinancement, si
l’État décidait d’aller dans ce sens. »
www.hceres.fr/fr/recherche...
« Ces recommandations sont impératives et devraient être satisfaites avant toute décision de refinancement, si
l’État décidait d’aller dans ce sens. »
www.hceres.fr/fr/recherche...
May 21, 2025 at 1:26 PM
[ #VeilleESR #LRU ] Rapport Hcéres sur l'IHU Méditerranée.
« Ces recommandations sont impératives et devraient être satisfaites avant toute décision de refinancement, si
l’État décidait d’aller dans ce sens. »
www.hceres.fr/fr/recherche...
« Ces recommandations sont impératives et devraient être satisfaites avant toute décision de refinancement, si
l’État décidait d’aller dans ce sens. »
www.hceres.fr/fr/recherche...
Je serais curieux de croiser les déclarations d'impôts avec les salaires moyens à la sortie annoncés par certaines formations.
April 30, 2025 at 11:29 AM
Je serais curieux de croiser les déclarations d'impôts avec les salaires moyens à la sortie annoncés par certaines formations.
C'est quand même bizarre que je ne puisse pas lire ce que mon ministre pense car c'est publié dans un journal auquel je n'ai pas accés.
April 14, 2025 at 8:21 AM
C'est quand même bizarre que je ne puisse pas lire ce que mon ministre pense car c'est publié dans un journal auquel je n'ai pas accés.
Si vous postulez à un poste de MCF/PU pensez à nommer vos fichiers de manière raisonnable avec un truc du style nom_prenon_dossier_poste_machin.pdf nom_prenom_carte_identite.pdf plutôt que main.pdf... les gens de Odyssée n'ont pas pensé à renommer les fichiers !
April 14, 2025 at 8:14 AM
Si vous postulez à un poste de MCF/PU pensez à nommer vos fichiers de manière raisonnable avec un truc du style nom_prenon_dossier_poste_machin.pdf nom_prenom_carte_identite.pdf plutôt que main.pdf... les gens de Odyssée n'ont pas pensé à renommer les fichiers !
Reposted by Julien Narboux
New in the AFP: Gyrovector Spaces
by F Marić and J Markovic
Gyrogroups and gyrovector spaces were introduced by Abraham A. Ungar and have deep connections to hyperbolic geometry and special relativity.
www.isa-afp.org/entries/Gyro...
by F Marić and J Markovic
Gyrogroups and gyrovector spaces were introduced by Abraham A. Ungar and have deep connections to hyperbolic geometry and special relativity.
www.isa-afp.org/entries/Gyro...
Formalization of Gyrovector Spaces as Models of Hyperbolic Geometry and Special Relativity
Formalization of Gyrovector Spaces as Models of Hyperbolic Geometry and Special Relativity in the Archive of Formal Proofs
www.isa-afp.org
April 9, 2025 at 3:24 PM
New in the AFP: Gyrovector Spaces
by F Marić and J Markovic
Gyrogroups and gyrovector spaces were introduced by Abraham A. Ungar and have deep connections to hyperbolic geometry and special relativity.
www.isa-afp.org/entries/Gyro...
by F Marić and J Markovic
Gyrogroups and gyrovector spaces were introduced by Abraham A. Ungar and have deep connections to hyperbolic geometry and special relativity.
www.isa-afp.org/entries/Gyro...
Reposted by Julien Narboux
A Barcelone, 2 000 modérateurs travaillant pour Facebook et Instagram licenciés
A Barcelone, 2 000 modérateurs travaillant pour Facebook et Instagram licenciés
Meta et son sous-traitant, Telus Digital, assurent que ces postes seront répartis sur d’autres sites.
www.lemonde.fr
April 4, 2025 at 9:12 AM
A Barcelone, 2 000 modérateurs travaillant pour Facebook et Instagram licenciés
Reposted by Julien Narboux
New in the AFP: Morley's Theorem
by B Puyobro
In any triangle, the three points of intersection of the adjacent angle trisectors form an equilateral triangle, called the Morley triangle. The proof is based on one by Alain Connes.
www.isa-afp.org/entries/Morl...
by B Puyobro
In any triangle, the three points of intersection of the adjacent angle trisectors form an equilateral triangle, called the Morley triangle. The proof is based on one by Alain Connes.
www.isa-afp.org/entries/Morl...
Morley's Theorem
Morley's Theorem in the Archive of Formal Proofs
www.isa-afp.org
April 2, 2025 at 5:20 PM
New in the AFP: Morley's Theorem
by B Puyobro
In any triangle, the three points of intersection of the adjacent angle trisectors form an equilateral triangle, called the Morley triangle. The proof is based on one by Alain Connes.
www.isa-afp.org/entries/Morl...
by B Puyobro
In any triangle, the three points of intersection of the adjacent angle trisectors form an equilateral triangle, called the Morley triangle. The proof is based on one by Alain Connes.
www.isa-afp.org/entries/Morl...
L'IA rend les formations à la va-vite encore moins pertinentes, le marché va avoir besoin surtout de gens hypers qualifiés, les formations courtes pour maitriser une techno sans recul ni capactié d'analyse seront de plus en plus inutiles.
March 18, 2025 at 5:55 PM
L'IA rend les formations à la va-vite encore moins pertinentes, le marché va avoir besoin surtout de gens hypers qualifiés, les formations courtes pour maitriser une techno sans recul ni capactié d'analyse seront de plus en plus inutiles.
Même quand tu enseignes ?
March 13, 2025 at 7:52 AM
Même quand tu enseignes ?
March 8, 2025 at 5:10 PM
Reposted by Julien Narboux
L'équité génère des frustrations, donc il faut embrasser les inégalités.
🙃
🙃
"Les mutations des professeurs, gérées par un barème commun dans un souci d’équité, génèrent des frustrations, car certaines zones en France sont plus attractives que d’autres.
Ce système interdit aussi de constituer des équipes autour d’un projet..."
www.lemonde.fr/idees/articl...
Ce système interdit aussi de constituer des équipes autour d’un projet..."
www.lemonde.fr/idees/articl...
Réformer le système de mutation des enseignants améliorerait l’école
ANALYSE. Les mutations des professeurs, gérées par un barème commun dans un souci d’équité, génèrent des frustrations, car certaines zones en France sont plus attractives que d’autres. Ce système inte...
www.lemonde.fr
March 3, 2025 at 7:57 PM
L'équité génère des frustrations, donc il faut embrasser les inégalités.
🙃
🙃
Reposted by Julien Narboux
Waterproof: Transforming a proof assistant into an educational tool. ~ Aalt Jelle Wemmenhove. research.tue.nl/nl/publicati... #ITP #Coq #Math #Education
Waterproof: Transforming a proof assistant into an educational tool
research.tue.nl
March 3, 2025 at 3:43 PM
Waterproof: Transforming a proof assistant into an educational tool. ~ Aalt Jelle Wemmenhove. research.tue.nl/nl/publicati... #ITP #Coq #Math #Education
Reposted by Julien Narboux
[ #VeilleESR #OperationPostes ] Un moteur de recherche super bien fichu des postes ATER, MCF et PR ouvertes au concours.
sciences.re/postes/
sciences.re/postes/
February 27, 2025 at 7:17 AM
[ #VeilleESR #OperationPostes ] Un moteur de recherche super bien fichu des postes ATER, MCF et PR ouvertes au concours.
sciences.re/postes/
sciences.re/postes/
Reposted by Julien Narboux
Machine-assisted proofs (February 19, 2025). ~ Terence Tao. youtu.be/5ZIIGLiQWNM #ITP #LeanProver #AI #Math
Terence Tao - Machine-Assisted Proofs (February 19, 2025)
YouTube video by Simons Foundation
youtu.be
February 21, 2025 at 6:17 PM
Machine-assisted proofs (February 19, 2025). ~ Terence Tao. youtu.be/5ZIIGLiQWNM #ITP #LeanProver #AI #Math
Reposted by Julien Narboux
Un salut nazi.
Voilà comment s'ouvre le congrès des conservateurs américains, avec Steve Bannon.
Depuis une semaine, Jordan Bardella y annonçait fièrement sa présence.
Que faut-il de plus pour ouvrir les yeux sur le danger que représente l’extrême-droite ?
Voilà comment s'ouvre le congrès des conservateurs américains, avec Steve Bannon.
Depuis une semaine, Jordan Bardella y annonçait fièrement sa présence.
Que faut-il de plus pour ouvrir les yeux sur le danger que représente l’extrême-droite ?
February 21, 2025 at 3:14 PM
Un salut nazi.
Voilà comment s'ouvre le congrès des conservateurs américains, avec Steve Bannon.
Depuis une semaine, Jordan Bardella y annonçait fièrement sa présence.
Que faut-il de plus pour ouvrir les yeux sur le danger que représente l’extrême-droite ?
Voilà comment s'ouvre le congrès des conservateurs américains, avec Steve Bannon.
Depuis une semaine, Jordan Bardella y annonçait fièrement sa présence.
Que faut-il de plus pour ouvrir les yeux sur le danger que représente l’extrême-droite ?
Reposted by Julien Narboux
ANNONCE : Aujourd'hui, 1ère émission d'une série de 4, soit le nombre d'articles d'Albert Einstein sortis en 1905.
À l’occasion des 120 ans de cette "année miraculeuse", c'est parti : la théorie des quanta, le mouvement brownien, la relativité restreinte et pour finir, la relation masse - énergie !
À l’occasion des 120 ans de cette "année miraculeuse", c'est parti : la théorie des quanta, le mouvement brownien, la relativité restreinte et pour finir, la relation masse - énergie !
February 19, 2025 at 11:24 AM
ANNONCE : Aujourd'hui, 1ère émission d'une série de 4, soit le nombre d'articles d'Albert Einstein sortis en 1905.
À l’occasion des 120 ans de cette "année miraculeuse", c'est parti : la théorie des quanta, le mouvement brownien, la relativité restreinte et pour finir, la relation masse - énergie !
À l’occasion des 120 ans de cette "année miraculeuse", c'est parti : la théorie des quanta, le mouvement brownien, la relativité restreinte et pour finir, la relation masse - énergie !
Pour le logiciel on a www.softwareheritage.org/save-referen...
How to save and reference research software - Software Heritage
A simple three-step process saves your code and provides a Software Heritage ID (SWHID) down to a single line.
www.softwareheritage.org
February 19, 2025 at 3:30 PM
Pour le logiciel on a www.softwareheritage.org/save-referen...