leanprover-community/mathlib4

Tracking Issue: Digraph Targets

Aperta

#26.771 aperta il 5 lug 2025

Vedi su GitHubGuida contributor
 (7 commenti) (1 reazione) (2 assegnatari)Lean (1592 fork)github user discovery
good first issuet-combinatorics

Metriche repository

Star
 (3869 stelle)
Metriche merge PR
 (Nessuna PR mergiata in 30 g)

Descrizione

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!

Guida contributor

Direzione di ricerca
Studia l'implementazione esistente di SimpleGraph in mathlib4 per comprenderne la struttura e i pattern, poi adattali per definire Digraph, connettività debole e forte e proprietà dei tornei.
Tech stack
Nessuno
Dominio
backend
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
3-5 giorni
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
GitLeanGraph theory
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
40