Teorema

De Viquipèdia
Dreceres ràpides: navegació, cerca
No s'ha de confondre amb «Teoria».
El teorema de Pitàgores té almenys 370 demostracions conegudes.[1]

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.[nota 1]

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ó[modifica | modifica el codi]

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 a 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.[2] En alguns casos, n'hi ha prou amb un diagrama per demostrar un teorema.[3][4]

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".[5][6] 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[modifica | modifica el codi]

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 a 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 de 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.

Un graf planar amb cinc colors tal que no hi ha dues regions adjacents amb el mateix color. Es pot demostrar que aquest mapa es pot acolorir amb només quatre colors. De fet, el teorema dels quatre colors afirma que, donat un graf planar qualsevol, n'hi ha prou amb quatre colors per acolorir el mapa de tal manera que no hi hagi dues regions adjacents amb el mateix color, però la demostració que se'n coneix implica una cerca computacional massa llarga per ser verificada manualment.

Alguns teoremes són "trivials", en el sentit que són una conseqüència immediata de les definicions, els axiomes i altres teiremes, 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.[7] 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.[8] Molts teoremes matemàtics es poden reduir a una computació més directa, com algunes identitats polinòmiques, trigonomètriques i hipergeomètriques.[9]

Enunciats i teoremes[modifica | modifica el codi]

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.[nota 2]

Relació amb teories científiques[modifica | modifica el codi]

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.

La conjectura de Collatz: una manera d'il·lustrar la seva complexitat és estendre la iteració dels nombres naturals als nombres complexos. El resultat és un fractal, que (d'acord amb la universalitat) s'assembla al conjunt de Mandelbrot.

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 × 1018. 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 1014 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 × 1040, que és aproximadament 10 elevat a 4,3 × 1039. Com que se suposa que el nombre de partícules de l'univers és menys de 10 elevat a 100 (un googol),[10] 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[modifica | modifica el codi]

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.[11] 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.[12]
  • 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ó.[13] 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.[14]
  • 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:

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[modifica | modifica el codi]

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[modifica | modifica el codi]

S'ha estimat que cada any es demostren més de 250.000 teoremes.[15]

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 se l'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 número de les seves col·laboracions, i la seva passió pel cafè.[16]

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ó.[17] 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[modifica | modifica el codi]

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 premises. 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.[18]

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.

Aquest diagrama il·lustra les entitats sintàctiques que es poden construir a partir dels llenguatges formals. Els símbols i les cadenes de símbols es poden dividir entre fórmules sense sentit i fórmules ben formades. Es pot pensar que un llenguatge formal és idèntic al conjunt de les seves fórmules ben formades. El conjunt de fórmules ben formades es pot dividir en aquelles que són teoremes i aquelles que no ho són.

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ó s'utilitza per indicar que és un teorema.

Els teoremes formals consisteixen de 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[modifica | modifica el codi]

Article principal: Semàntica formal

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[modifica | modifica el codi]

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 . 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 amb una longitud finita i d'un mínim de 3 simbols és una fórmula. No hi cap altre tipus de formula.»

L'únic axioma de és:

ABBA.

L'única regla d'inferència per és:

«Qualsevol aparició de "A" en un teorema es pot substituir per la cadena "AB" i el resultat és un teorema.»

Els teoremes de es defineixen com aquelles fórmules que tenen una derivació que finalitza amb la fórmula en qüestió. Per exemple,

  1. ABBA (Donada com a axioma)
  2. ABBBA (aplicant la regla d'inferència)
  3. ABBBAB (aplicant la regla d'inferència)

és una derivació. Per tant, "ABBBAB" és un teorema de . 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 són:

  • Tot teorema comença amb "A".
  • Tot teorema té exactament dues "A".

Notes[modifica | modifica el codi]

  1. 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"
  2. Vegeu [1] i [2] Noia 64 mimetypes pdf.pngPDF
  3. 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[modifica | modifica el codi]

  1. 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].
  2. Lee, John M. «Some Remarks on Writing Mathematical Proofs» (Noia 64 mimetypes pdf.pngPDF). University of Washington Mathematics Department. [Consulta: 14 setembre 2016].
  3. Nelsen, 1997.
  4. Nelsen, 2000.
  5. Gauss, Carl Friedrich. (traducció de Griselda Pascual Xufré). Disquisicions aritmètiques. Institut d'Estudis Catalans, 1996, p. 160. ISBN 9788472833135. 
  6. Domènech i Mira, Josep. Moviments Educatius Actuals. Editorial Visión Libros, 2012, p. 240-241. ISBN 9788490115558. 
  7. Weisstein, Eric W., «Deep Theorem» a MathWorld (en anglès).
  8. Zeilberger, Doron. «Opinion 51».
  9. Petkovšek; Wilf; Zeilberger, 1996, p. 6.
  10. Heile, Frank «How many particles are there in the universe?». Quora, 29-07-2012 [Consulta: 20 setembre 2016].
  11. Wentworth; Smith, 1913, Art. 46, 47.
  12. Wentworth; Smith, 1913, Art. 50.
  13. Wentworth; Smith, 1913, Art. 51.
  14. Wentworth; Smith, 1913, Art. 79.
  15. Hoffman, 1998, p. 204.
  16. Hoffman, 1998, p. 7.
  17. Elwes, Richard. «An enormous theorem: the classification of finite simple groups». Plus Magazine, número 41, desembre 2006.
  18. Hofstadter, 1980, p. 60, «(anglès) ...in a formal system, the theorems are predefined, by the rules of production.».

Bibliografia[modifica | modifica el codi]

Bibliografia addicional[modifica | modifica el codi]

  • 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. 

Vegeu també[modifica | modifica el codi]

Portal

Portal: Matemàtiques

Enllaços externs[modifica | modifica el codi]

A Wikimedia Commons hi ha contingut multimèdia relatiu a: Teorema Modifica l'enllaç a Wikidata
  • 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