Des intuitions aux épreuves

La méthode

Explorer une idée.
Savoir ce qu’elle établit.

Une image peut ouvrir une piste. Une preuve établit une relation. Une mesure confronte une proposition au réel. La méthode FLUX précise le rôle de chacune.

Le fil d’une recherche

Chaque passage demande
son argument.

« Ce qui ne se referme pas, c’est ce qui avance. »

Une ambition ouverte.
Des exigences explicites.

01 / Donner sa portée à chaque phrase

Six statuts.
Six façons de lire.

Le Tome Zéro distingue six catégories. Elles disent quel rôle joue un énoncé et ce qui permet de l’évaluer. Les numéros sont des repères de lecture, pas des notes de confiance.

T0

Une définition ou une convention

Fixer le sens des mots avant de raisonner.

Le texte précise un objet, une notation ou une règle de départ. Deux lecteurs doivent pouvoir comprendre la même chose lorsqu’ils l’utilisent.

Exemple de formulation« Nous appelons écart la différence entre ces deux quantités, définies de cette manière. »

Ce que l’on doit pouvoir consulter

Une définition précise, son domaine d’utilisation et les conventions retenues.

La portée à garder en tête

Définir un objet permet de travailler avec lui. Son existence dans la nature demande un argument distinct.

T1

Un théorème démontré

Établir une conclusion à partir d’hypothèses explicites.

La démonstration porte sur un énoncé précis, avec ses objets et ses conditions. Elle doit permettre de suivre pourquoi la conclusion découle de ce qui a été posé.

Exemple de formulation« Sous les hypothèses annoncées, cette relation est démontrée pour tous les cas du domaine défini. »

Ce que l’on doit pouvoir consulter

L’énoncé exact, la preuve et ses hypothèses. Si une certification formelle est annoncée, les éléments permettant de la vérifier.

La portée à garder en tête

La portée de la preuve est celle de l’énoncé démontré. Le lien avec une interprétation physique doit être établi séparément.

T2

Un résultat à consolider

Distinguer ce qui tient déjà de ce qui reste à compléter.

Un argument cohérent ou une construction avancée peut orienter le travail alors que sa vérification n’est pas entièrement achevée. Le point restant doit être nommé.

Exemple de formulation« Cette étape est établie ; la justification du passage suivant ou sa vérification formelle reste à compléter. »

Ce que l’on doit pouvoir consulter

La partie acquise, la limite exacte et le travail nécessaire pour la lever.

La portée à garder en tête

La solidité d’une partie du raisonnement ne suffit pas à valider automatiquement l’ensemble.

T3

Une conjecture ouverte

Formuler une idée assez précise pour pouvoir la travailler.

Des indices, une régularité ou une intuition forte suggèrent une relation. La démonstration reste à construire, et les objections possibles font partie de la recherche.

Exemple de formulation« Une même règle pourrait organiser ces structures. Voici la relation à démontrer et les cas à examiner. »

Ce que l’on doit pouvoir consulter

Une proposition précise, les indices qui la motivent et les obstacles encore présents.

La portée à garder en tête

Une conjecture peut guider la recherche. Elle garde son caractère ouvert lorsqu’un raisonnement s’appuie sur elle.

T4

Une projection vers les phénomènes

Relier une construction à ce que l’on peut observer.

Une proposition physique, biologique ou cosmologique fait correspondre les objets du cadre à des phénomènes. Elle doit préciser comment cette correspondance pourrait être testée.

Exemple de formulation« Cette règle devrait permettre de calculer une grandeur mesurable. Voici les données et les conditions de comparaison. »

Ce que l’on doit pouvoir consulter

Une quantité observable, les entrées du calcul, les incertitudes et un résultat qui conduirait à revoir la proposition.

La portée à garder en tête

Une proposition sans test disponible doit rester explicitement spéculative. Un accord avec des données ne suffit pas à expliquer à lui seul l’origine de la règle.

T5

Une image pour comprendre

Donner une prise à l’intuition.

Une métaphore rapproche une idée abstraite d’une expérience familière. Elle aide à imaginer et à poser une question ; le raisonnement doit ensuite préciser ce qu’il en retient.

Exemple de formulation« Une porte entrouverte peut évoquer ce qui reste ouvert et appelle une suite. »

Ce que l’on doit pouvoir consulter

Le sens de l’analogie et le point où la comparaison cesse de s’appliquer.

La portée à garder en tête

Une image ne porte pas de preuve. Pour devenir une proposition de recherche, elle doit être traduite en objets et en relations précis.

Les exemples servent à comprendre les catégories. Ils n’annoncent aucun résultat de recherche particulier.

Repère du corpus : Tome Zéro, § 0.3. Un même projet peut contenir plusieurs statuts ; chacun s’attache à un énoncé précis.

02 / Suivre le raisonnement

Trois vérifications
qui se complètent.

Avant de demander si une proposition est convaincante, on peut regarder ce qu’elle dit, comment elle est construite et ce qui permet de la mettre à l’épreuve.

  1. 01

    L’énoncé

    Qu’est-ce qui est réellement proposé ?

    Une phrase précise, les objets concernés et les limites de la question. Une affirmation sur certains cas ne devient pas une affirmation sur tous les cas.

  2. 02

    Le raisonnement

    Pourquoi la conclusion suivrait-elle ?

    Les définitions, les hypothèses et chaque étape utile. Un calcul sur de nombreux exemples donne des indications ; sa portée dépend de ce qui a effectivement été vérifié.

  3. 03

    L’observation

    À quoi confronter la proposition ?

    Pour une lecture physique, une quantité mesurable, une méthode de comparaison et les incertitudes. La correspondance entre l’objet mathématique et la mesure fait elle aussi partie du travail.

Un résultat vérifiable laisse une trace : la version du texte, les hypothèses, les données, le calcul ou la preuve, et ce qui reste ouvert.

03 / Comprendre d’où vient un nombre

Un même accord.
Des démarches différentes.

Une valeur calculée peut être très proche d’une mesure. Pour comprendre ce que cet accord apporte, il faut aussi savoir comment la règle a été obtenue.

Ajuster

Choisir à partir des données.

On règle un ou plusieurs paramètres pour décrire des mesures connues. C’est un ajustement, dont les choix et les limites doivent rester visibles.

Prévoir

Fixer la règle avant le test.

On confronte une règle à des données qui n’ont pas servi à la construire ou à la régler. Le test apporte une information nouvelle sur sa portée.

Déduire

Établir pourquoi la règle suit.

On démontre qu’un résultat découle des principes et des hypothèses annoncés. Si une valeur mesurée entre dans le calcul, elle reste une entrée à déclarer.

Ces démarches peuvent se compléter. Les distinguer permet de savoir ce que l’accord explique, et ce qu’il laisse encore à comprendre.

04 / Lire une fiche de recherche

Une galaxie.
Une question précise.

Sur la page des trois échelles, les mouvements d’une galaxie servent de point d’entrée. Voici comment transformer cette idée en une fiche que l’on pourrait examiner.

Exemple de démarche · Projection T4

À construire et à tester

La règle proposée retrouve-t-elle
les vitesses de rotation observées ?

Cette fiche illustre la méthode. Elle ne présente pas un résultat obtenu sur une galaxie particulière.

La quantité comparée
La vitesse de rotation en fonction de la distance au centre, sur un intervalle défini.
Les entrées du calcul
Les informations utilisées sur la matière visible et toutes les autres données nécessaires. Chaque paramètre ajusté doit être déclaré.
La règle annoncée
La relation utilisée, ses hypothèses et son domaine de validité. Elle est fixée avant d’examiner les données réservées au test.
La confrontation
Les écarts entre calcul et mesures, en tenant compte des incertitudes et d’une comparaison menée dans les mêmes conditions.
Ce qui ferait revoir la proposition
Un désaccord persistant au-delà des incertitudes, selon un critère défini à l’avance. Les cas difficiles font partie du résultat.
Comprendre une courbe de rotation

05 / La vérification formelle

Lean : vérifier le raisonnement,
avec ses hypothèses.

Lean est un assistant de preuve. On y écrit des objets, un énoncé et une démonstration dans un langage précis. Son noyau vérifie que la preuve est acceptée dans le cadre formel déclaré.

Ce que l’on vérifie.

L’énoncé exact, les définitions employées et les hypothèses dont la preuve dépend. Une certification doit pouvoir être reproduite sur les fichiers concernés.

Le Tome Zéro demande notamment de rendre consultables les axiomes, les dépendances et le lien entre le texte et l’énoncé formalisé.

Le lien avec la nature.

Il faut expliquer comment les objets du raisonnement correspondent aux phénomènes, puis confronter cette interprétation aux observations.

Une relation peut être mathématiquement établie tandis que son interprétation physique reste une question de recherche.

Pourquoi les hypothèses comptent-elles autant ?

Si une propriété est posée au départ, les résultats qui l’utilisent en dépendent. La vérification formelle permet d’examiner ces dépendances ; elle ne rend pas vraie, par elle-même, une hypothèse choisie.

Les axiomes sont les principes admis dans le cadre. Les expliciter permet de savoir exactement sur quoi repose une démonstration.

06 / Faire une place à l’objection

Un résultat qui résiste
fait avancer le travail.

Le corpus conserve une leçon de méthode : dans un cas étudié, une vérification numérique confirmait la conclusion sans valider l’argument utilisé. Il fallait reprendre la preuve.

« Vérifier la conclusion ne vérifie pas la preuve. »
Catalogue de l’établi · § F16.7, « Leçon de méthode »

Une objection utile désigne le point précis qui pose problème : une hypothèse cachée, un cas oublié, un calcul irréalisable ou un désaccord avec des mesures. La réponse consiste à corriger, restreindre ou reclasser la proposition, en conservant la trace de ce qui a changé.

Le Tome Astres demande également de garder les tests qui échouent dans l’historique. Ils indiquent où une piste rencontre sa limite et orientent la suite du travail.

Sources et repères de lecture

Cette page propose une lecture accessible des exigences formulées dans le corpus. Elle décrit une méthode et n’atteste pas, à elle seule, que chaque résultat du programme satisfait déjà toutes ces exigences.

  • Tome Zéro, §§ 0.2–0.3 : sens des mots et hiérarchie des six statuts ; §§ 0.11–0.12 : confrontation empirique et rôle de Lean.
  • Mathematica Universalis — Plan directeur complet de fermeture, § 37 : distinction entre identité, calibration, ajustement, prédiction et reconnaissance numérique.
  • Catalogue de l’établi — MU / FLUX, § F16.7 : vérifier la conclusion et vérifier la preuve ; § F17 : rendre explicites les choix et leurs alternatives.
  • Tome Astres, préambule « Méthode » : entrées déclarées, statuts et conservation des tests négatifs.

Pour examiner le fonctionnement de l’outil lui-même : documentation officielle de Lean sur la validation des preuves (en anglais, lecture facultative).