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.
Une petite pensée pour ses proches .
August 3, 2025 at 7:03 AM
Une petite pensée pour ses proches .
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...
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...
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 !
Reposted by Julien Narboux
Automating math (Computers can already help verify proofs. One day soon, AI may be able to come up with new ones). ~ Adam Marblestone. asteriskmag.com/issues/09/au... #ITP #LeanProver #AI #LLMs #Math
Automating Math—Asterisk
Computers can already help verify proofs. One day soon, AI may be able to come up with new ones.
asteriskmag.com
February 19, 2025 at 6:35 AM
Automating math (Computers can already help verify proofs. One day soon, AI may be able to come up with new ones). ~ Adam Marblestone. asteriskmag.com/issues/09/au... #ITP #LeanProver #AI #LLMs #Math
Reposted by Julien Narboux
Un article dans @lemonde.fr sur la vérification informatique et formelle de la preuve du théorème de Fermat et sur la collaboration internationale menée par Kevin Bizzard
www.lemonde.fr/sciences/art...
www.lemonde.fr/sciences/art...
February 18, 2025 at 5:46 AM
Un article dans @lemonde.fr sur la vérification informatique et formelle de la preuve du théorème de Fermat et sur la collaboration internationale menée par Kevin Bizzard
www.lemonde.fr/sciences/art...
www.lemonde.fr/sciences/art...
Reposted by Julien Narboux
Goedel-Prover: A new frontier in automated theorem proving. ~ Yong Lin et als. goedel-lm.github.io #LLMs #ITP #LeanProver
Goedel-Prover Goedel-Prover: Pushing the Limits of Automated Theorem Proving Through Large-Scale Data Synthesis
Pushing the Limit of Automated Theorem Proving Through Large Scale Data Synthesizing
goedel-lm.github.io
February 5, 2025 at 12:02 PM
Goedel-Prover: A new frontier in automated theorem proving. ~ Yong Lin et als. goedel-lm.github.io #LLMs #ITP #LeanProver
Reposted by Julien Narboux
STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. arxiv.org/abs/2502.00212 #LLMs #ITP #LeanProver #IsabelleHOL
STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
A fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data. Although reinforcement learning or expert iteration partially mitigates this issue by alternating b...
arxiv.org
February 12, 2025 at 7:08 AM
STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. arxiv.org/abs/2502.00212 #LLMs #ITP #LeanProver #IsabelleHOL
Reposted by Julien Narboux
Teaching and learning proof in mathematics at university: new perspectives in education with proof assistants? ~ Cécile Ouvrier-Buffet. hal.science/hal-04838823... #ITP #Math #Education
December 24, 2024 at 7:50 AM
Teaching and learning proof in mathematics at university: new perspectives in education with proof assistants? ~ Cécile Ouvrier-Buffet. hal.science/hal-04838823... #ITP #Math #Education
Reposted by Julien Narboux
Foundations of proof assistants: impact on student perception of proof. ~ Iro Bartzia, Emmanuel Beffara, Antoine Meyer, Julien Narboux. hal.science/hal-04227823... #ITP #Teaching
October 17, 2023 at 10:19 AM
Foundations of proof assistants: impact on student perception of proof. ~ Iro Bartzia, Emmanuel Beffara, Antoine Meyer, Julien Narboux. hal.science/hal-04227823... #ITP #Teaching
According to arxiv.org/pdf/2311.03755 it seems that some LLM has learned that for producing an Isabelle formalization, one should ask to Manuel Eberl :-)
February 14, 2025 at 8:11 AM
According to arxiv.org/pdf/2311.03755 it seems that some LLM has learned that for producing an Isabelle formalization, one should ask to Manuel Eberl :-)
Reposted by Julien Narboux
Vous aimez les maths? Nous on adore. C'est pourquoi Epsiloon est heureux de s'associer avec le prestigieux Institut Henri Poincaré. La "maison des maths", à Paris, se propose d'offrir aux visiteurs des articles sur l’actu de la recherche. Son Comité en a sélectionné 6 dans Epsiloon. Grosse fierté…
February 12, 2025 at 7:26 AM
Vous aimez les maths? Nous on adore. C'est pourquoi Epsiloon est heureux de s'associer avec le prestigieux Institut Henri Poincaré. La "maison des maths", à Paris, se propose d'offrir aux visiteurs des articles sur l’actu de la recherche. Son Comité en a sélectionné 6 dans Epsiloon. Grosse fierté…
Reposted by Julien Narboux
