leanprover-community/batteries

Verify Binary Heap

Ouverte

#1 442 ouverte le 2 oct. 2025

Voir sur GitHub
 (5 commentaires) (0 réaction) (0 personne assignée)Lean (154 forks)auto 404
enhancementhelp wanted

Métriques du dépôt

Stars
 (406 étoiles)
Métriques de merge PR
 (Merge moyen 7j 15h) (26 PRs mergées en 30 j)

Description

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!

Guide contributeur

Direction de recherche
Étudiez l'implémentation existante de BinaryHeap dans Batteries/Data/BinaryHeap.lean et comprenez les bases du prouveur de théorèmes Lean. Développez ensuite une preuve de vérification formelle pour les propriétés du tas.
Stack technique
Aucun
Domaine
data
Type d'issue
Recherche
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
Une demi journée
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
Git
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
60