leanprover-community/batteries

Verify Binary Heap

Aperta

#1442 aperta il 2 ott 2025

Vedi su GitHub
 (5 commenti) (0 reazioni) (0 assegnatari)Lean (154 fork)auto 404
enhancementhelp wanted

Metriche repository

Star
 (406 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

This is a standard textbook algorithm. It is well implemented in Batteries.Data.BinaryHeap but not verified.

If you're looking to get started with formal verification project in Lean, this should be an interesting one to try!

Guida contributor

Direzione di ricerca
Studia l'implementazione esistente di BinaryHeap in Batteries/Data/BinaryHeap.lean e comprendi le basi del dimostratore di teoremi Lean. Quindi sviluppa una prova di verifica formale per le proprietà dello heap.
Tech stack
Nessuno
Dominio
data
Tipo issue
Ricerca
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
Mezza giornata
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Git
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
60