leanprover-community/mathlib4

Tracking Issue: Digraph Targets

Open

#26,771 opened on Jul 5, 2025

View on GitHub
 (7 comments) (1 reaction) (2 assignees)Lean (1,381 forks)github user discovery
good first issuet-combinatorics

Repository metrics

Stars
 (3,405 stars)
PR merge metrics
 (No merged PRs in 30d)

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!

Contributor guide

Research direction
Study the existing SimpleGraph implementation in mathlib4 to understand the structure and patterns, then adapt them to define Digraph, weak and strong connectivity, and tournament properties.
Tech stack
None
Domain
backend
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
3-5 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
GitLeanGraph theory
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
40