leanprover-community/mathlib4

Tracking Issue: Digraph Targets

Offen

#26.771 geöffnet am 05.07.2025

Auf GitHub ansehenContributor Guide
 (7 Kommentare) (1 Reaktion) (2 zugewiesene Personen)Lean (1.592 Forks)github user discovery
good first issuet-combinatorics

Repository-Metriken

Stars
 (3.869 Sterne)
PR-Merge-Metriken
 (Keine gemergten PRs in 30 T)

Beschreibung

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!

Contributor Guide

Research-Richtung
Studieren Sie die vorhandene SimpleGraph Implementierung in mathlib4, um die Struktur und Muster zu verstehen, und passen Sie sie dann an, um Digraph, schwache und starke Konnektivität sowie Turniereigenschaften zu definieren.
Tech Stack
Keine
Domain
backend
Issue Type
Funktion
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
3
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
3-5 Tage
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Aktiv
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
GitLeanGraph theory
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
40