An Entity of Type: language, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

Lean is a theorem prover and programming language. It is based on the calculus of constructions with inductive types. The Lean project is an open source project, hosted on GitHub. It was launched by Leonardo de Moura at Microsoft Research in 2013. Lean has an interface that differentiates it from other interactive theorem provers. Lean can be compiled to JavaScript and accessed in a web browser. It has native support for Unicode symbols. (These can be typed using LaTeX-like sequences, such as " imes" for "×".) Lean also has an extensive support for meta-programming.

Property Value
dbo:abstract
  • Lean Theorem Prover Lean est un assistant de preuve et un langage de programmation. Il repose sur le principe de calcul des constructions avec . 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 " imes"). 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 et Kevin Buzzard . 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. Ces 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. -. (fr)
  • Lean is a theorem prover and programming language. It is based on the calculus of constructions with inductive types. The Lean project is an open source project, hosted on GitHub. It was launched by Leonardo de Moura at Microsoft Research in 2013. Lean has an interface that differentiates it from other interactive theorem provers. Lean can be compiled to JavaScript and accessed in a web browser. It has native support for Unicode symbols. (These can be typed using LaTeX-like sequences, such as " imes" for "×".) Lean also has an extensive support for meta-programming. Lean has gotten attention from mathematicians Thomas Hales and Kevin Buzzard. Hales is using it for his project, Formal Abstracts. Buzzard uses it for the Xena project. One of the Xena Project's goals is to rewrite every theorem and proof in the undergraduate math curriculum of Imperial College London in Lean. (en)
  • Lean — инструмент интерактивного доказательства теорем. Основан на исчислении конструкций с индуктивными типами. Имеет открытый исходный код, размещенный на GitHub. Проект Lean был запущен Леонардо де Моурой в Microsoft Research в 2013 году. Lean имеет интерфейс, который отличает его от других интерактивных средств доказательства теорем. Lean может быть скомпилирован на JavaScript и доступен в веб-браузере. Он имеет встроенную поддержку символов Юникода. (Они могут быть набраны с использованием последовательностей, подобных применяемым в системе LaTeX, таких как " imes" для "×".) Lean также имеет обширную поддержку метапрограммирования. (ru)
dbo:developer
dbo:influencedBy
dbo:latestReleaseDate
  • 2022-09-17 (xsd:date)
dbo:latestReleaseVersion
  • 3.48.0
dbo:license
dbo:thumbnail
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 62889984 (xsd:integer)
dbo:wikiPageLength
  • 5246 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1119615259 (xsd:integer)
dbo:wikiPageWikiLink
dbp:developer
dbp:genre
dbp:influencedBy
dbp:language
  • English (en)
dbp:latestPreviewDate
  • 2022-08-07 (xsd:date)
dbp:latestPreviewVersion
  • 4 (xsd:integer)
dbp:latestReleaseDate
  • 2022-09-17 (xsd:date)
dbp:latestReleaseVersion
  • 3.480000 (xsd:double)
dbp:license
dbp:logo
  • Lean logo2.svg (en)
dbp:logoSize
  • 220 (xsd:integer)
dbp:name
  • Lean (en)
dbp:operatingSystem
dbp:paradigm
dbp:programmingLanguage
  • C++, Lean (en)
dbp:repo
  • Preview: (en)
  • Stable: (en)
dbp:typing
dbp:website
  • Preview: (en)
  • Stable: (en)
dbp:wikiPageUsesTemplate
dcterms:subject
rdf:type
rdfs:comment
  • Lean is a theorem prover and programming language. It is based on the calculus of constructions with inductive types. The Lean project is an open source project, hosted on GitHub. It was launched by Leonardo de Moura at Microsoft Research in 2013. Lean has an interface that differentiates it from other interactive theorem provers. Lean can be compiled to JavaScript and accessed in a web browser. It has native support for Unicode symbols. (These can be typed using LaTeX-like sequences, such as " imes" for "×".) Lean also has an extensive support for meta-programming. (en)
  • Lean Theorem Prover Lean est un assistant de preuve et un langage de programmation. Il repose sur le principe de calcul des constructions avec . 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 " imes"). 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 possi (fr)
  • Lean — инструмент интерактивного доказательства теорем. Основан на исчислении конструкций с индуктивными типами. Имеет открытый исходный код, размещенный на GitHub. Проект Lean был запущен Леонардо де Моурой в Microsoft Research в 2013 году. (ru)
rdfs:label
  • Lean (assistant de preuve) (fr)
  • Lean (proof assistant) (en)
  • Lean (ru)
owl:sameAs
prov:wasDerivedFrom
foaf:depiction
foaf:homepage
foaf:isPrimaryTopicOf
foaf:name
  • Lean (en)
foaf:page
is dbo:influencedBy of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:influencedBy of
is owl:differentFrom of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License