Lean (assistant de preuve)


Lean Theorem Prover
Description de l'image Lean logo2.svg.

Informations
Développé par Microsoft Research
Première version
Dernière version 4.13.0 ()[1]Voir et modifier les données sur Wikidata
Dépôt https://github.com/leanprover/lean
Écrit en C++
Système d'exploitation MultiplateformeVoir et modifier les données sur Wikidata
Environnement Dans le navigateur ou cross-platform
Formats lus Lean 3 file format (d) et Lean 4 file format (d)Voir et modifier les données sur Wikidata
Formats écrits Lean 3 file format (d) et Lean 4 file format (d)Voir et modifier les données sur Wikidata
Langues Anglais
Type Assistant de preuve
Licence Apache 2.0
Site web https://leanprover.github.io

Lean est un assistant de preuve et un langage de programmation. Il repose sur le principe de calcul des constructions avec types inductifs.

Lean possède un certain nombre de fonctionnalités notables qui le distinguent des autres logiciels d'assistance à la preuve. Lean peut être compilé vers du JavaScript, et est ainsi accessible dans un navigateur Web. Il prend en charge nativement les caractères Unicode des symboles mathématiques, qui peuvent être saisis grâce à des raccourcis rappelant la syntaxe de LaTeX (par exemple, "×" s'obtient en tapant "\times"). Il est également possible de faire de la méta-programmation en utilisant le même langage que pour une utilisation classique. Ainsi, si l'utilisateur veut écrire une fonction qui prouve automatiquement certains théorèmes, il est possible d'écrire en Lean une fonction générant les preuves voulues en Lean.

Lean a retenu l'attention des mathématiciens Thomas Hales [2] et Kevin Buzzard [3]. Hales l'utilise pour son projet Formal Abstracts. Buzzard l'utilise pour le projet Xena, dont l'un des objectifs est de réécrire en Lean chaque théorème et preuve du programme de premier cycle en mathématiques de l'Imperial College London.

Cet assistant de preuve a été écrit principalement par Leonardo de Moura. Ses fondements logiques sont presque identiques à ceux de Coq (logiciel). Sa bibliothèque mathématique est élaborée collectivement, par environ 250 contributeurs. Cette bibliothèque donne une assise commune aux projets de validation. En 2022, si tout le programme de l'Agrégation de mathématiques n'y est pas encore entré, les espaces perfectoïdes ou l'espace topologique de Bourbaki y sont présents. -[4].

Exemples

Voici comment les nombres naturels sont définis dans Lean :

inductive nat : Type
| zero : nat
| succ : nat  nat

Voici la définition de l'addition pour les nombres naturels :

definition add : nat  nat  nat
| n zero     := n
| n (succ m) := succ(add n m)

Voici une simple preuve en Lean :

theorem and_swap : p  q  q  p :=
    assume h1 : p  q,
    h1.right, h1.left

Voici la même preuve en utilisant des tactics :

theorem and_swap (p q : Prop) : p  q  q  p :=
begin
    assume h : (p  q), -- on suppose que p ∧ q est vrai
    cases h, -- on extrait les propositions individuelles de la conjonction
    split, -- on sépare le but à prouver en deux cas : prouver p et prouver q séparément
    repeat { assumption }
end

Références

  1. « Release 4.13.0 », (consulté le )
  2. Hales, « A Review of the Lean Theorem Prover » (consulté le )
  3. Buzzard, « The Future of Mathematics? » (consulté le )
  4. Patrick Massot, « Pourquoi raconter des maths à un ordinateur », sur www.larecherche.fr (consulté le )

Liens externes

Read other articles:

Governor of New Jersey from 1982 to 1990 For his son, see Thomas Kean Jr. For other persons with similar names, see Tom Kean (disambiguation). Thomas KeanKean in 2018President of the Carnegie Corporation of New YorkActingApril 15, 2021 – January 2023Served with Janet L. RobinsonPreceded byVartan GregorianSucceeded byLouise RichardsonChair of the 9/11 CommissionIn officeDecember 15, 2002 – August 21, 2004PresidentGeorge W. BushDeputyLee HamiltonPreceded byHenry KissingerS...

 

la Riolle Caractéristiques Longueur 11,4 km Bassin collecteur Loire Régime pluvial Cours · Localisation La Chapelle-Blanche-Saint-Martin · Altitude 116 m · Coordonnées 47° 06′ 51″ N, 0° 46′ 02″ E Confluence la Ligoire · Localisation Bournan · Altitude 61 m · Coordonnées 47° 03′ 01″ N, 0° 41′ 54″ E Géographie Pays traversés France Département Indre-et-Loire Régions traversées Centre-V...

 

2022 film by Alice Diop Saint OmerTheatrical release posterDirected byAlice DiopScreenplay by Alice Diop Amrita David Marie NDiaye Produced by Toufik Ayadi Christophe Barral Starring Kayije Kagame Guslagie Malanda Valérie Dréville Aurélia Petit Xavier Maly Robert Canterella Salimata Kamate Thomas de Pourquery CinematographyClaire MathonEdited byAmrita DavidMusic byThibault DeboaisneProductioncompanySrab FilmsDistributed byLes Films du losangeRelease dates 7 September 2022 (2...

Letak Cary di Carolina Utara Cary merupakan sebuah kota di Amerika Serikat. Kota ini letaknya di bagian timur. Tepatnya di negara bagian Carolina Utara. Pada tahun 2010, kota ini memiliki jumlah penduduk sebesar 135.234 jiwa dan memiliki luas wilayah 112,6 km². Kota ini memiliki angka kepadatan penduduk sebesar 1.213,5 jiwa/km². Pranala luar Wikimedia Commons memiliki media mengenai Cary, North Carolina. Situs resmi Cary Chamber of Commerce Cary Downtown - Heart of Cary Artikel bertopi...

 

Bola tenis Bola tenis adalah bola yang dirancang untuk olahraga tenis. Bola tenis berwarna kuning fluoresens pada acara olahraga besar,[1][2] tetapi dalam permainan rekreasi bisa berwarna apa saja. Bola tenis ditutupi dengan serat berserat yang memodifikasi sifat aerodinamisnya, dan masing-masing memiliki lekukan lonjong melengkung putih yang menutupinya. Bola tenis diisi dengan udara dan permukaannya ditumbuhi oleh kompon karet berserat seragam. Keterlambatan terasa pemisahan...

 

Paruh-bajak gelambir Eulacestoma nigropectus Status konservasiRisiko rendahIUCN22705592 TaksonomiKerajaanAnimaliaFilumChordataKelasAvesOrdoPasseriformesFamiliCorvidaeGenusEulacestomaSpesiesEulacestoma nigropectus De Vis, 1894 Tipe taksonomiEulacestoma lbs Paruh-bajak gelambir ( Eulacestoma nigropectus ) adalah burung kecil dari papua . Ia adalah satu-satunya anggota genus monotaip Eulacestoma dan keluarga Eulacestomatidae . Ia juga dikenal sebagai gelatik-bentet gelambir.[2] Keteranga...

† Человек прямоходящий Научная классификация Домен:ЭукариотыЦарство:ЖивотныеПодцарство:ЭуметазоиБез ранга:Двусторонне-симметричныеБез ранга:ВторичноротыеТип:ХордовыеПодтип:ПозвоночныеИнфратип:ЧелюстноротыеНадкласс:ЧетвероногиеКлада:АмниотыКлада:Синапсиды�...

 

Botanical garden in Emmarentia, Johannesburg, South Africa Johannesburg Botanical GardenThe Rose Garden in the Johannesburg Botanical GardenTypeBotanical gardenLocationJohannesburg, South AfricaCoordinates26°9′9″S 28°0′10″E / 26.15250°S 28.00278°E / -26.15250; 28.00278Area81 hectares (200 acres)Elevation1605mCreated1968Operated byJohannesburg City ParksOpen6am - 6pmCamp sitesnoHiking trailsnoPlants20,000 trees2,500 succulentsCollections5,532ParkingyesW...

 

Haircut Blowout (haircut) redirects here. For the process to get sleek hair, see Blowout (hairstyle). This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Temple fade hairstyle – news · newspapers · books · scholar · JSTOR (June 2012) (Learn how and when to remove this message) The temple fade haircut has sh...

Agency of the U.S. Department of Agriculture Natural Resources Conservation ServiceAgency overviewFormedSeptember 13, 1933Preceding agencySoil Conservation Service, Soil Erosion ServiceHeadquartersWashington, D.C.EmployeesApprox 11,000Agency executiveTerry Cosby, ChiefParent agencyDepartment of AgricultureWebsitewww.nrcs.usda.gov Natural Resources Conservation Service (NRCS), formerly known as the Soil Conservation Service (SCS), is an agency of the United States Department of Agriculture (US...

 

Северный морской котик Самец Научная классификация Домен:ЭукариотыЦарство:ЖивотныеПодцарство:ЭуметазоиБез ранга:Двусторонне-симметричныеБез ранга:ВторичноротыеТип:ХордовыеПодтип:ПозвоночныеИнфратип:ЧелюстноротыеНадкласс:ЧетвероногиеКлада:АмниотыКлада:Синапси...

 

Voce principale: Promozione 1955-1956. La Promozione fu il massimo campionato regionale di calcio disputato in Toscana nella stagione 1955-1956. A ciascun girone, che garantiva al suo vincitore la promozione in IV Serie a condizione di soddisfare le condizioni economiche richieste dai regolamenti, partecipavano sedici squadre, ed era prevista la retrocessione delle quattro peggio piazzate, anche se erano possibili aggiustamenti automatici per ripartire fra le appropriate sedi locali le squad...

Dario Venitucci Nazionalità  Italia Altezza 173 cm Peso 67 kg Calcio Ruolo Centrocampista Squadra  Clivense CarrieraGiovanili 199?-???? Paradiso Collegno1999-2007 JuventusSquadre di club1 2006-2007 Juventus5 (0)2007-2008 Treviso30 (2)2008-2009 Mantova5 (0)2009 Avellino16 (1)2009-2010 Arezzo29 (3)[1]2010-2011 Bassano Virtus27 (1)2011-2012 Foggia22 (5)2012-2013 Carrarese22 (1)2013-2014 Foggia30 (4)2014-2015 Barletta29 (4...

 

Sebuah rawa rawa di Jurong East Untuk melihat penggunaan lain dari Jurong lihat Jurong (disambiguasi) Jurong East ialah sebuah kota kecil yang terletak hampir dekat Clementi yang meliputi 380 hektare tanah di Singapura Barat. Persimpangan MRT dan bus di Jurong East juga terletak di sini. Plus, yang terkenal Singapore Science Centre juga terletak di sini di mana wisatawan berkumpul tiap hari. Singapore Science Center agak dekat ke Singapore Chinese Gardens atau Yu Hua Yuan. Keduanya terletak d...

 

National park in South Carolina, United States Congaree National ParkIUCN category Ib (wilderness area)[1]Boardwalk passes through old growth forest of bald cypress and water tupeloLocation in South CarolinaShow map of South CarolinaCongaree National Park (the United States)Show map of the United StatesLocationRichland County, South Carolina, United StatesNearest cityEastover, South Carolina (town)Coordinates33°47′0″N 80°47′0″W / 33.78333°N 80.78333°W&...

  提示:此条目页的主题不是俄台關係法。 《臺灣關係法》全名本法乃為協助維持西太平洋之和平、安全與穩定,並授權美国人民与台湾人民继续保持商业、文化和其他关系,以促進美國外交政策,並為其他目的。缩写(通俗)TRA立法机构第96屆美国国会生效日期1979年1月1日引用文献公法美國聯邦公法第96–8號法律汇编93 Stat. 14法典编纂修订法编美國法典第22卷...

 

Artikel ini sebatang kara, artinya tidak ada artikel lain yang memiliki pranala balik ke halaman ini.Bantulah menambah pranala ke artikel ini dari artikel yang berhubungan atau coba peralatan pencari pranala.Tag ini diberikan pada November 2022. Fella El Djazairiaفلة الجزائريةفلة الجزائريةInformasi latar belakangNama lahirFella Abd al-Hamid Ababsaفلة عبد الحميد عبابسةNama lainFella El DjazairiaLahir23 April 1961 (umur 63)Saint-Denis, PrancisGenre...

 

Austrian footballer Dijon Kameri Kameri with Liefering in 2021Personal informationDate of birth (2004-04-20) 20 April 2004 (age 20)Place of birth Burgenland, AustriaHeight 1.81 m (5 ft 11 in)[1]Position(s) MidfielderTeam informationCurrent team Red Bull SalzburgNumber 8Youth career2012–2016 Liefering2016–2017 Red Bull Salzburg2017–2018 Liefering2018–2021 Red Bull SalzburgSenior career*Years Team Apps (Gls)2021–2022 Liefering 30 (3)2022– Red Bull Salzbur...

1971 British film by Malcolm Leigh Games That Lovers PlayPromotional posterDirected byMalcolm LeighWritten byMalcolm LeighProduced byJudith SmithStarringJoanna LumleyPenny BrahmsRichard WattisCinematographyKen HigginsEdited byPeter Austen-HuntMusic byDavid LindupProductioncompanyBorder Film ProductionsRelease date 14 March 1971 (1971-03-14) Running time95 minutesCountryUnited KingdomLanguageEnglish Games That Lovers Play (U.S. titles: Lady Chatterley Versus Fanny Hill and Lady ...

 

Selección de fútbol de la República Dominicana Datos generalesPaís República DominicanaCódigo FIFA DOMFederación Federación Dominicana de FútbolConfederación ConcacafSeudónimo(s) Los quisqueyanosSeleccionador  Marcelo Neveleff (desde 2023)Capitán Tano Bonnín Más goles Jonathan Faña (24)Clasificación FIFA 150.º (julio de 2024)Estadio(s) Estadio Olímpico Félix Sánchez, Santo DomingoEquipaciones Primera Segunda Primer partido República Dominicana 0:8 HaitíSanto Domingo...