# Teorema

En matemàtiques, un teorema és una clàusula o proposició que es pot demostrar vertadera en un marc lògic determinat, format, per exemple, per altres teoremes, i per enunciats generalment acceptats, com els axiomes. Un teorema és una conseqüència lògica dels axiomes. La demostració de teoremes és una activitat central en matemàtiques, i consisteix en un argument lògic de l'enunciat del teorema, basat en les regles d'un sistema deductiu. La demostració d'un teorema s'acostuma a interpretar com una justificació de la veracitat de l'enunciat del teorema. Segons la manera en què es demostren els teoremes, el concepte de teorema és fonamentalment deductiu, en contrast amb la noció d'una llei científica, que és experimental.
Cal no confondre teorema i teoria. En matemàtiques, un conjunt de teoremes i de definicions (axiomes) pot formar una teoria, com la teoria de nombres.

## Descripció

Molts teoremes matemàtics tenen la forma d'enunciats condicionals. En aquest cas, la demostració arriba a la conclusió a partir de certes condicions anomenades hipòtesis o premisses. Quan s'interpreta la demostració com una justificació de la veracitat, s'acostuma a veure la conclusió com una conseqüència necessària de les hipòtesis, és a dir, la conclusió és certa en el cas que les hipòtesis siguin certes, sense cap supòsit addicional. Tanmateix, el condicional es pot interpretar d'una manera diferent en certs sistemes deductius, depenent dels significats atribuïts a les regles de derivació i al símbol condicional.
Encara que es poden expressar en una forma completament simbòlica, per exemple, en termes de càlcul proposicional, els teoremes s'acostumen a expressar en un llenguatge natural; anàlogament per a les demostracions, que s'acostumen a expressar com a arguments informals organitzats de manera lògica, amb l'objectiu de convèncer els lectors de la veracitat de l'enunciat del teorema, fora de cap dubte, i a partir de la qual se'n podria construir, en principi, una demostració simbòlica. Aquests arguments en llenguatge natural són més senzills de comprovar que els expressats en forma purament simbòlica; de fet, molts matemàtics expressen la seva preferència per demostracions que no només mostrin la validesa d'un teorema, sinó que també expliquin per què són certes. En alguns casos, n'hi ha prou amb un diagrama per demostrar un teorema.
Com que els teoremes són una part central de les matemàtiques, també pot hom considerar la seva estètica. Alguns teoremes es cataloguen com a "trivials", o "difícils", o "profunds", o fins i tot amb "bellesa". Aquestes apreciacions subjectives poden variar, no només de persona a persona, sinó també amb el temps: per exemple, quan se simplifica o s'entén millor una demostració, un teorema que es considerava difícil ara es pot veure com a trivial. D'altra banda, un teorema profund pot tenir un enunciat senzill, però la seva demostració pot implicar connexions sorprenents i subtils entre diferents àrees de les matemàtiques. El darrer teorema de Fermat és un exemple ben conegut d'aquest tipus de teoremes.

## Tipologia de teoremes

Des d'un punt de vista de la lògica, molts teoremes tenen la forma d'un indicatiu condicional: «si A, llavors B». Aquest enunciat no afirma B, només que B és una conseqüència necessària d'A. En aquest cas, hom diu que A és hipòtesi del teorema (cal notar que, aquí, "hipòtesi" és quelcom diferent d'una conjectura) i B la conclusió (formalment, A i B són l'antecedent i el conseqüent). El teorema «Si n és un nombre natural parell, llavors n/2 és un nombre natural» és un exemple típic en el qual la hipòtesi és «n és un nombre natural parell» i la conclusió és «n/2 també és un nombre natural».
Per tal de ser demostrat, un teorema s'ha de poder expressar com un enunciat formal i precís. Tanmateix, els teoremes s'acostumen a expressar en un llenguatge natural en comptes d'en forma completament simbòlica, amb l'objectiu de què el lector pugui crear un enunciat formal a partir de l'informal.
És habitual en matemàtiques escollir un cert nombre d'hipòtesis en un cert llenguatge i declarar que la teoria consisteix en tots els enunciats demostrables a partir d'aquestes hipòtesis. Aquestes hipòtesis configuren la base fonamental de la teoria, i s'anomenen axiomes o postulats. L'àrea de les matemàtiques coneguda com a teoria de la demostració estudia els llenguatges formals, els axiomes i l'estructura de les demostracions.
Alguns teoremes són "trivials", en el sentit que són una conseqüència immediata de les definicions, els axiomes i altres teoremes, i no contenen sorpreses. D'altra banda, altres teoremes es consideren "profunds", ja que les seves demostracions poden ser llargues i complicades, o poden implicar àrees de les matemàtiques sense connexió aparent amb l'enunciat del teorema, o poden connectar diferents àrees de les matemàtiques de manera sorprenent. Un teorema pot ser profund encara que el seu enunciat sigui simple; un exemple d'aquest cas és el Darrer Teorema de Fermat, però n'hi ha d'altres en teoria de nombres i combinatòria.
Altres teoremes tenen una demostració coneguda que no es pot escriure de manera simple. Els exemples més coneguts de teoremes d'aquest tipus són el teorema dels quatre colors i la conjectura de Kepler. S'ha demostrat que aquests dos teoremes són certs reduint-los a una cerca computacional que llavors es comprova mitjançant un programa d'ordinador. Inicialment, molts matemàtics no acceptaven aquest tipus de demostració, però actualment està més acceptada. El matemàtic Doron Zeilberger afirmà que aquests són, possiblement, els únics resultats no trivials que han demostrat mai els matemàtics. Molts teoremes matemàtics es poden reduir a una computació més directa, com algunes identitats polinòmiques, trigonomètriques i hipergeomètriques.

## Enunciats i teoremes

Estrictament parlant, per tal d'establir un enunciat matemàtic com a teorema, en cal una demostració, és a dir, una seqüència d'arguments lògics que parteixen dels axiomes del sistema (i d'altres teoremes existents –i demostrats– anteriorment), fins a arribar com a conclusió a l'enunciat que es vol demostrar. No obstant això, s'acostumen a considerar per separat la demostració del teorema. Encara que pot haver-hi més d'una demostració per a un teorema, només cal una demostració per tal que l'enunciat es consideri un teorema. El teorema de Pitàgores i la llei de reciprocitat quadràtica competeixen per ser el teorema amb el nombre més gran de demostracions diferents.

## Relació amb teories científiques

Els teoremes de les matemàtiques i les teories de les ciències són fonamentalment diferents en la seva epistemologia. Una teoria científica no es pot demostrar; el seu atribut clau és que és refutable, és a dir, fa prediccions sobre el món natural que són verificables mitjançant experiments. Qualsevol incoherència entre la predicció i l'experiment mostra que la teoria científica és incorrecta, o almenys limita la seva precisió o el seu àmbit de validesa. Els teoremes matemàtics, per altra banda, són enunciats formals purament abstractes: la demostració d'un teorema no pot implicar experiments ni cap altra prova experimental.
Tanmateix, hi ha cert grau d'empirisme i recol·lecció de dades implicats en el descobriment de teoremes matemàtics. Si s'identifica un patró, de vegades amb l'ajut d'un ordinador potent, els matemàtics poden tenir una idea de què s'ha de demostrar, i en alguns casos fins i tot un pla per confeccionar la demostració. Per exemple, s'ha verificat la conjectura de Collatz amb valors inicials de fins a aproximadament 2,88 × 10$^{18}$. La hipòtesi de Riemann s'ha verificat per als primers 10 bilions de zeros de la funció zeta. Cap d'aquests enunciats es considera demostrat.
Aquestes verificacions no constitueixen una demo. Per exemple, la conjectura de Mertens és un enunciat sobre nombres naturals que ara se sap que és fals, però no se'n coneix cap contraexemple explícit (és a dir, un nombre natural n per al qual la funció de Mertens M(n) és igual o superior a l'arrel quadrada de n): tots els nombres més petits que 10¹⁴ tenen la propietat de Mertens, i només es coneix que el nombre més petit que no té aquesta propietat és menor que l'exponencial d'1,59 × 10$^{40}$, que és aproximadament 10 elevat a 4,3 × 10$^{39}$. Com que se suposa que el nombre de partícules de l'Univers és menys de 10 elevat a 100 (un googol), no s'espera trobar un contraexemple explícit mitjançant una cerca per força bruta.
Cal notar que el terme "teoria" també existeix en matemàtiques, per denotar un conjunt d'axiomes matemàtics, definicions i teoremes, com per exemple, la teoria de grups. També hi ha "teoremes" en ciències, particularment en física i en enginyeria, però sovint tenen enunciats i demostracions on les suposicions físiques i la intuïció juguen un rol important: els axiomes físics sobre els quals es basen aquests "teoremes" són, de fet, refutables.

## Terminologia

Existeixen diversos termes per als diferents enunciats matemàtics; aquests termes indiquen el rol que juguen aquests enunciats en una àrea de coneixement determinada. La distinció entre els diferents termes és, de vegades, arbitrària, i l'ús d'alguns termes ha evolucionat amb el temps.
* Un axioma o postulat és un enunciat acceptat sense demostració i vist com a fonamental per a una certa àrea de coneixement. Històricament eren considerats com a "evidents per si mateixos", però més recentment es consideren com a suposicions que caracteritzen l'objecte d'estudi. En geometria clàssica, els axiomes són enunciats generals, mentre que els postulats són enunciats sobre objectes geomètrics. Una definició també s'accepta sense demostració perquè només proporciona el significat d'una paraula o frase en termes de conceptes coneguts.
* Un enunciat sense demostrar que se suposa cert s'anomena conjectura (o de vegades hipòtesi, però amb un sentit diferent del qual s'ha vist anteriorment). Per tal de ser considerat com a conjectura, l'enunciat s'ha de proposar públicament, moment en el qual es pot afegir el nom del proponent a la conjectura, com en el cas de la conjectura de Goldbach. Altres conjectures famoses són la conjectura de Collatz i la hipòtesi de Riemann. D'altra banda, el darrer teorema de Fermat sempre s'ha conegut com a teorema, fins i tot quan no se'n coneixia la demostració; mai no va ser conegut com la "conjectura de Fermat".
* Una proposició és un teorema sense cap importància especial. Aquest terme denota de vegades un enunciat amb una demostració senzilla, mentre que s'acostuma a reservar el terme teorema per a resultats més importants o per a aquells amb demostracions llargues o difícils. En geometria clàssica, una proposició pot ser una construcció que satisfà uns certs requisits; per exemple, la Proposició 1 del Llibre I dels Elements d'Euclides és la construcció d'un triangle equilàter.
* Un lema és un "teorema auxiliar", una proposició que es pot aplicar d'una manera limitada, excepte com a part de la demostració d'un teorema més ampli. En alguns casos, i segons es feia més clara la importància relativa de diferents teoremes, allò que una vegada es considerava un lema ara es considera un teorema, encara que es mantingui el terme "lema" al títol de l'enunciat. Alguns exemples són el lema de Gauss, el lema de Zorn i el lema fonamental.
* Un corol·lari és una proposició que és una conseqüència immediata d'un altre teorema o definició, amb una petita demostració. També s'utilitza el terme corol·lari per a un teorema reformulat per a un cas especial més restringit. Per exemple, el teorema que afirma que tots els angles d'un rectangle són rectes admet un corol·lari: tots els angles d'un quadrat (un cas especial de rectangle) són rectes.
* El recíproc d'un teorema és un enunciat format per l'intercanvi d'allò donat en el teorema i d'allò que es vol demostrar. Per exemple, el teorema del triangle isòsceles afirma que, si dos costats d'un triangle són iguals, llavors dos angles són iguals. En el recíproc, s'intercanvien allò donat (que dos costats són iguals) i allò que es vol demostrar (que dos angles són iguals), de tal manera que l'enunciat recíproc és que si dos angles d'un triangle són iguals, llavors dos costats són iguals. En aquest exemple, es pot demostrar que el recíproc és un altre teorema, però en general això no és cert. Per exemple, el recíproc del teorema que afirma que dos angles rectes són iguals és l'enunciat que afirma que dos angles iguals han de ser angles rectes, la qual cosa clarament no és certa.
* Una generalització és un teorema que inclou un altre teorema demostrat anteriorment com a cas especial i, per tant, el primer és un corol·lari del segon.
Existeixen altres termes, menys utilitzats, que estan vinculats a certs enunciats demostrats, de tal manera que hom acostuma a anomenar aquests teoremes pels seus noms històrics. Per exemple:
* Una identitat és una igualtat, dins d'un teorema, entre dues expressions matemàtiques, que resulta certa independentment dels valors particulars que s'utilitzin per a qualsevol de les variables o paràmetres que apareixen en les expressions. Alguns exemples són la fórmula d'Euler i la identitat de Vandermonde.
* Una regla és un teorema, com la regla de Bayes o la regla de Cramer, que estableix una fórmula útil.
* Una llei o un principi és un teorema que resulta vàlid en un ampli ventall de circumstàncies. Alguns exemples són la llei dels grans nombres, la llei del paral·lelogram, la llei zero-u de Kolmogórov, el principi de Harnack i el principi de les caselles.
Alguns teoremes tenen una altra terminologia. L'algorisme de la divisió (vegeu Divisió euclidiana) és un teorema que expressa el resultat d'una divisió en el conjunt dels nombres naturals i en anells més generals. La identitat de Bézout és un teorema que afirma que el màxim comú divisor de dos nombres es pot escriure com a combinació lineal d'aquests dos nombres. La paradoxa de Banach-Tarski és un teorema en l'àmbit de la teoria de la mesura que resulta paradoxal, en el sentit que contradiu la intuïció habitual sobre volums en l'espai tridimensional.

## Estructura

L'estructura típica d'un teorema i la seva demostració és la següent:
    Teorema (nom de la persona que el va demostrar i any de descobriment, demostració o publicació).
    Enunciat del teorema (de vegades anomenat «proposició»).
    Demostració.
    Descripció de la demostració.
    Marca final.
El final de la demostració es pot indicar amb les lletres Q.E.D. (quod erat demonstrandum) o amb algun dels signes de final d'article "□" o "∎", introduïts per Paul Halmos a partir del seu ús en articles publicats.
L'estil concret depèn de l'autor o de la publicació. Moltes publicacions proporcionen instruccions o macros en el seu llibre d'estil per a la confecció de textos matemàtics.
És habitual trobar, abans d'un teorema, les definicions que descriuen el significat exacte dels termes que s'utilitzen. També és habitual precedir un teorema amb diverses proposicions o lemes que s'utilitzaran posteriorment en la demostració. Tanmateix, de vegades els lemes es troben enmig de la demostració del teorema, bé amb demostracions a continuació de cada lema, o bé amb demostracions presentades després de la demostració del teorema.
Els corol·laris d'un teorema es poden situar o bé entre el teorema i la demostració, o bé directament després de la demostració. De vegades, els corol·laris tenen demostracions pròpies que expliquen perquè són una conseqüència del teorema.

## Cultura popular

S'ha estimat que cada any es demostren més de 250.000 teoremes.
El conegut aforisme "Un matemàtic és una màquina per transformar cafè en teoremes" es deu probablement a Alfréd Rényi, encara que sovint s'atribueix al company de Rényi Paul Erdős (i Rényi podria estar pensant en Erdős), que era famós per la gran quantitat de teoremes que va trobar, el nombre de les seves col·laboracions, i la seva passió pel cafè.
La classificació dels grups simples finits es considera com una de les demostracions més llargues d'un teorema. Està formada per desenes de milers de pàgines en uns 500 articles publicats per uns 100 autors. Hom considera que la recopilació d'aquestes publicacions configura una demostració completa, i hi ha diversos projectes en curs que tenen l'objectiu de simplificar aquesta demostració. Un altre teorema d'aquest tipus és el teorema dels quatre colors, que té una demostració per ordinador massa llarga per ser lleguda per humans. De fet, és la demostració més llarga coneguda per a un enunciat comprensible per a un humà.

## Teoremes en lògica

La lògica, especialment en l'àmbit de la teoria de la demostració, considera els teoremes com a enunciats (anomenats fórmules o fórmules ben formades) d'un llenguatge formal. Els enunciats dels teoremes són cadenes de símbols, i es poden dividir en fórmules sense sentit i fórmules ben formades. També cal proporcionar un conjunt de regles de deducció, també anomenades regles de transformació o regles d'inferència. Aquestes regles de deducció ens diuen exactament quan es pot derivar una fórmula a partir d'un conjunt de premisses. El conjunt de fórmules ben formades es pot dividir entre aquelles que són teoremes i aquelles que no ho són. Tanmateix, segons Hofstadter, és habitual que un sistema formal defineixi simplement totes les seves fórmules ben formades com a teoremes.
Si s'escullen diferents conjunts de regles de derivació, es donen lloc a diferents interpretacions del que significa que una expressió sigui un teorema. L'objectiu d'algunes regles de derivació i llenguatges formals és capturar el raonament matemàtic; els exemples més comuns utilitzen la lògica de primer ordre. Altres sistemes deductius descriuen la reescriptura de termes, com per exemple les regles de reducció per al càlcul λ.
La definició de teoremes com a elements d'un llenguatge formal permet obtenir resultats de teoria de la demostració que estudien l'estructura de les demostracions formals i l'estructura de les fórmules demostrables. El resultat més conegut és el primer teorema d'incompletesa de Gödel; en representar els teoremes de la teoria de nombres bàsica com a expressions d'un llenguatge formal, i en representar llavors aquest llenguatge dins de la pròpia teoria de nombres, Gödel va construir exemples d'enunciats que no són ni demostrables ni refutables a partir de les axiomatitzacions de la teoria de nombres.
Un teorema es pot expressar en un llenguatge formal (o "formalitzat"). Un teorema formal és l'anàleg purament formal d'un teorema. En general, un teorema formal és un tipus de fórmula ben formada que satisfà certes condicions lògiques i sintàctiques. La notació $\vdash S$ s'utilitza per indicar que $S$ és un teorema.
Els teoremes formals consisteixen en fórmules d'un llenguatge formal i de les regles de transformació d'un sistema formal. Específicament, un teorema formal és sempre l'última fórmula d'una derivació en algun sistema formal, on cada fórmula de la derivació és una conseqüència lògica de les fórmules que apareixen amb anterioritat dins la derivació. Les fórmules acceptades inicialment en la derivació s'anomenen axiomes, i són la base sobre la qual es deriva el teorema. Un conjunt de teoremes s'anomena teoria.
El que fa útils i interessants als teoremes formals és que es poden interpretar com a proposicions certes i les seves derivacions es poden interpretar com una demostració de la veracitat de l'expressió resultant. Un conjunt de teoremes formals es pot anomenar teoria formal. Un teorema la interpretació del qual és un enunciat cert sobre un sistema formal s'anomena metateorema.

### Sintaxi i semàntica

El concepte d'un teorema formal és fonamentalment sintàctic, en contrast amb la noció de proposició certa, que introdueix la semàntica. Sistemes deductius diferents poden donar lloc a diferents interpretacions, depenent de les suposicions de les regles de derivació (és a dir, creença, justificació o altres modalitats). La solidesa d'un sistema formal depèn de si la totalitat dels seus teoremes són també valideses. Una validesa és una fórmula que és certa sota qualsevol interpretació possible; per exemple, en lògica proposicional clàssica, les valideses són les tautologies. Es considera que un sistema formal és semànticament complet quan totes les seves tautologies són també teoremes.

### Derivació d'un teorema

La noció de teorema està íntimament lligada a la seva demostració formal (també anomenada "derivació"). Per il·lustrar com es confeccionen les derivacions, tindrem com a exemple un sistema formal molt simplificat, diem-ne ${\mathcal {FS}}$. El seu alfabet consta només de dos símbols { A, B }, i la seva regla de formació per a fórmules és:
    «Tota cadena de símbols de ${\mathcal {FS}}$ amb una longitud finita i d'un mínim de 3 símbols és una fórmula. No hi cap altre tipus de formula.»
L'únic axioma de ${\mathcal {FS}}$ és:
    ABBA.
L'única regla d'inferència per ${\mathcal {FS}}$ és:
    «Qualsevol aparició de "A" en un teorema es pot substituir per la cadena "AB" i el resultat és un teorema.»
Els teoremes de ${\mathcal {FS}}$ es defineixen com aquelles fórmules que tenen una derivació que finalitza amb la fórmula en qüestió. Per exemple,
* ABBA (Donada com a axioma)
* ABBBA (aplicant la regla d'inferència)
* ABBBAB (aplicant la regla d'inferència)
és una derivació. Per tant, "ABBBAB" és un teorema de ${\mathcal {FS}}$. Tanmateix, no es pot aplicar la noció de veritat (o falsedat) a la fórmula "ABBBAB" fins que no es doni una interpretació als seus símbols. Així, en aquest exemple, la fórmula encara no representa una proposició, sinó que és merament una abstracció buida de contingut.
Dos metateoremes de ${\mathcal {FS}}$ són:
* Tot teorema comença amb "A".
* Tot teorema té exactament dues "A".

## Bibliografia

* Heath, Sir Thomas Little. The works of Archimedes. Dover, 1897 [Consulta: 11 setembre 2016].
* Hoffman, Paul. The Man Who Loved Only Numbers: The Story of Paul Erdős and the Search for Mathematical Truth. Nova York: Hyperion, 1998. ISBN 1-85702-829-5.
* Hofstadter, Douglas. Gödel, Escher, Bach: An Eternal Golden Braid ( PDF). Basic Books, 1979.
* Hunter, Geoffrey. Metalogic: An Introduction to the Metatheory of Standard First Order Logic. University of California Press, 1996. ISBN 0-520-02356-0.
* Mates, Benson. Elementary Logic. Oxford University Press, 1972. ISBN 0-19-501491-X.
* Petkovšek, Marko; Wilf, Herbert S.; Zeilberger, Doron. A = B. Wellesley, Massachusetts: A.K. Peters, 1996. ISBN 1-56881-063-6 [Consulta: 26 setembre 2016]. Arxivat 2006-01-29 a Wayback Machine.
* Wentworth, G.; Smith, D.E.. Plane Geometry. Ginn & Co., 1913.

## Notes

* ↑ Tot i això, tant els teoremes com les lleis científiques són el resultat d'investigacions. Vegeu Heath 1897, Introduction, The terminology of Archimedes "teorema (θεὼρνμα), de θεωρεἳν, investigar"
* ↑ Vegeu i PDF
* ↑ La paraula llei també es pot referir a un axioma, una regla d'inferència, o, en teoria de la probabilitat, una distribució de probabilitat.

## Referències

* ↑ Elisha Scott Loomis. «The Pythagorean proposition: its demonstrations analyzed and classified, and bibliography of sources for data of the four kinds of proofs». Education Resources Information Center. Institute of Education Sciences (IES) of the U.S. Department of Education. [Consulta: 11 setembre 2016].
* ↑ Lee, John M. «Some Remarks on Writing Mathematical Proofs» ( PDF). University of Washington Mathematics Department. [Consulta: 14 setembre 2016].
* ↑ Nelsen, 1997.
* ↑ Nelsen, 2000.
* ↑ Gauss, Carl Friedrich. (traducció de Griselda Pascual Xufré). Disquisicions aritmètiques. Institut d'Estudis Catalans, 1996, p. 160. ISBN 9788472833135.
* ↑ Domènech i Mira, Josep. Moviments Educatius Actuals. Editorial Visión Libros, 2012, p. 240-241. ISBN 9788490115558.
* ↑ Weisstein, Eric W., «Deep Theorem» a MathWorld (en anglès).
* ↑ Zeilberger, Doron. «Opinion 51».
* ↑ Petkovšek, Wilf i Zeilberger, 1996, p. 6.
* ↑ Wentworth i Smith, 1913, Art. 46, 47.
* ↑ Wentworth i Smith, 1913, Art. 50.
* ↑ Wentworth i Smith, 1913, Art. 51.
* ↑ Wentworth i Smith, 1913, Art. 79.
* ↑ Hoffman, 1998, p. 204.
* ↑ Hoffman, 1998, p. 7.
* ↑ Elwes, Richard. «An enormous theorem: the classification of finite simple groups». Plus Magazine, número 41, desembre 2006.
* ↑ Hofstadter, 1980, p. 60, «(anglès) ...in a formal system, the theorems are predefined, by the rules of production.».

## Vegeu també

* Corol·lari
* Demostració matemàtica
* Gödel, Escher, Bach
* Inferència
* Lema (matemàtiques)

## Bibliografia addicional

* Nelsen, Roger B. Proofs without Words: Exercises in Visual Thinking. Mathematical Association of America, 1997. ISBN 978-0-88385-700-7.
* Nelsen, Roger B. Proofs without Words II: More Exercises in Visual Thinking. Mathematical Association of America, 2000. ISBN 0-88385-721-9.

## Enllaços externs

* Weisstein, Eric W., «Theorem» a MathWorld (en anglès).
* Theorem of the Day (anglès)
* Metamath – un llenguatge per a desenvolupar definicions i demostracions matemàtiques estrictament formals, acompanyat d'un verificador de demostracions per a aquest llenguatge i d'una base de dades creixent de milers de teoremes demostrats