| 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. (fr)
- 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. (fr)
|
| dbo:computingPlatform
| |
| dbo:developer
| |
| dbo:latestReleaseDate
| |
| dbo:latestReleaseVersion
| |
| dbo:license
| |
| dbo:type
| |
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 4118 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| prop-fr:art
| |
| prop-fr:dateDeDernièreVersion
| |
| prop-fr:dateDePremièreVersion
| |
| prop-fr:dernièreVersion
| |
| prop-fr:dépôt
| |
| prop-fr:développeur
|
- Microsoft Research (fr)
- Microsoft Research (fr)
|
| prop-fr:environnement
|
- Dans le navigateur ou cross-platform (fr)
- Dans le navigateur ou cross-platform (fr)
|
| prop-fr:id
| |
| prop-fr:lang
| |
| prop-fr:langageDeProgrammation
| |
| prop-fr:langues
|
- Anglais (fr)
- Anglais (fr)
|
| prop-fr:licence
|
- Apache 2.0 (fr)
- Apache 2.0 (fr)
|
| prop-fr:nom
|
- Lean Theorem Prover (fr)
- Lean Theorem Prover (fr)
|
| prop-fr:siteWeb
| |
| prop-fr:type
|
- Assistant de preuve (fr)
- Assistant de preuve (fr)
|
| prop-fr:wikiPageUsesTemplate
| |
| dct:subject
| |
| rdf:type
| |
| rdfs:comment
|
- 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 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)
|
| rdfs:label
|
- Lean (assistant de preuve) (fr)
- Lean (proof assistant) (en)
|
| rdfs:seeAlso
| |
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:homepage
| |
| foaf:isPrimaryTopicOf
| |
| foaf:name
|
- (fr)
- Lean Theorem Prover (fr)
- (fr)
- Lean Theorem Prover (fr)
|
| is dbo:wikiPageDisambiguates
of | |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is oa:hasTarget
of | |
| is foaf:primaryTopic
of | |
