leanprover-community/mathlib4

Tracking Issue: Digraph Targets

Ouverte

#26 771 ouverte le 5 juil. 2025

Voir sur GitHubGuide contributeur
 (7 commentaires) (1 réaction) (2 personnes assignées)Lean (1 592 forks)github user discovery
good first issuet-combinatorics

Métriques du dépôt

Stars
 (3 869 étoiles)
Métriques de merge PR
 (Aucune PR mergée en 30 j)

Description

This is a list of things related to digraphs that would be nice to have.

  • Weak and strong connectivity.

    • If vertices have equal in-degree and out-degree, then the digraph is weakly connected if and only if it is strongly connected.
    • Robbin's Theorem.

  • Tournaments

    • A tournament has a Hamiltonian path.
    • A tournament has a Hamiltonian cycle If and only if it is strongly connected.

Many of the concepts that already exist in SimpleGraph should be ported to Digraph too. Feel free to add digraph results that you would like to see formalized!

Guide contributeur

Direction de recherche
Étudiez l'implémentation existante de SimpleGraph dans mathlib4 pour comprendre la structure et les motifs, puis adaptez les pour définir Digraph, la connectivité faible et forte, et les propriétés des tournois.
Stack technique
Aucun
Domaine
backend
Type d'issue
Fonctionnalité
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.
3-5 jours
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
GitLeanGraph theory
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
40