Preverjanje kromatičnega števila grafov z dokazovalnim pomočnikom Lean : delo diplomskega seminarja

Kikelj, Gregor (author), Bauer, Andrej (mentor), Berčič, Katja (comentor)

V dokazovalniku in programskem jeziku Lean 4 formaliziramo osnove teorije grafov, barvanj in kromatičnega števila. Implementiramo tudi dokazano pravilen algoritem za računanje kromatičnega števila ter analiziramo čas izvajanja. Na koncu implementiramo in dokažemo pravilnost algoritma za preverjanje 2-obarvljivosti v polinomskem času.

• Language: Slovenian
• Keywords: Lean, Lean 4, graf, kromatično število
• Work type: Final seminar paper
• Typology: 2.11 - Undergraduate Thesis
• Organization: FMF - Faculty of Mathematics and Physics
• Year: 2024
• PID: 20.500.12556/RUL-163092
• UDC: 004
• COBISS.SI-ID: 209899011
• Publication date in RUL: 02.10.2024

Secondary language

• Language: English
• Title: Verification of the chromatic number of a graph with the Lean proof assistant

Abstract

In the Lean 4 proof assistant and programming language, we formalize the basics of graph theory, colorings, and chromatic numbers. We also implement a proven correct algorithm for computing the chromatic number and analyze its running time. Finally, we implement and prove the correctness of an algorithm for checking 2-colorability in polynomial time.

• Keywords: Lean, Lean 4, graph, chromatic number