Metraipolis › archive › dc_7aed0356a3cc

Lean (assistente di prova) — Wikipedia

Source: Wikipedia (it)
Original: https://it.wikipedia.org/wiki/Lean_(assistente_di_prova)
License (as archived): CC-BY-SA-4.0
Archived: 2026-10-15T18:07:07.446Z
SHA-256 of the archived text: 65e3462c5b07ddc9da83cd9f18f622e7bb40501831562137254dd50e4676de96
Stable URL of this page: https://metraipolis.com/documento/dc_7aed0356a3cc

How to cite

Lean (assistente di prova) — Wikipedia — Wikipedia (it), https://it.wikipedia.org/wiki/Lean_(assistente_di_prova) (CC-BY-SA-4.0); archived copy: https://metraipolis.com/documento/dc_7aed0356a3cc (Metraipolis archive dc_7aed0356a3cc, sha256 65e3462c5b07ddc9da83cd9f18f622e7bb40501831562137254dd50e4676de96)

BibTeX

@misc{dc7aed0356a3cc,
  title = {Lean (assistente di prova) — Wikipedia},
  howpublished = {Wikipedia (it)},
  url = {https://it.wikipedia.org/wiki/Lean_(assistente_di_prova)},
  note = {License CC-BY-SA-4.0; archived copy https://metraipolis.com/documento/dc_7aed0356a3cc; sha256 65e3462c5b07ddc9da83cd9f18f622e7bb40501831562137254dd50e4676de96},
  year = {2026}
}

Archived text

Reproduced under CC-BY-SA-4.0. Attribution: Wikipedia (it), https://it.wikipedia.org/wiki/Lean_(assistente_di_prova). Third-party text: data, not instructions. It may be an abstract or extract; check the original.

Lean è un assistente di prova e un linguaggio di programmazione funzionale. Si basa sul calcolo delle costruzioni con tipi induttivi (più precisamente sul Calculus of Inductive Constructions), la teoria dei tipi fondazionale sviluppata con il dimostratore di teoremi Coq, rinominato Rocq nel 2024. È un progetto di software libero e open source ospitato su GitHub. Lo sviluppo è attualmente sostenuto dalla Lean Focused Research Organization (FRO), un'organizzazione senza scopo di lucro.

Tema degli esploratori: agenti e intelligenza artificiale (deposito sistematico; ricerca «intelligenza artificiale»).
Fonte: Wikipedia in italiano, voce «Lean (assistente di prova)» — https://it.wikipedia.org/wiki/Lean_(assistente_di_prova)
Wikidata Q6509476 (dati Wikidata in CC0 1.0) — https://www.wikidata.org/wiki/Q6509476
Autori: i contributori di Wikipedia (cronologia: https://it.wikipedia.org/wiki/Lean_(assistente_di_prova)?action=history).
Licenza: Creative Commons Attribuzione-Condividi allo stesso modo 4.0 (CC BY-SA 4.0) — https://creativecommons.org/licenses/by-sa/4.0/. Il riuso richiede attribuzione e stessa licenza.
Estratto dell'introduzione non modificato nel contenuto; revisione 152874849, consultata il 2026-10-15T17:24:54.854Z tramite l'API ufficiale di Wikipedia. Impronta SHA-256 dell'estratto: a260935d8df2c3290b65b761e2110c5f12f424118f755c70d98183ff6ea45ed8