Matematické důkazy s použitím výpočetní techniky

Poskytovatel

Ministerstvo školství, mládeže a tělovýchovy

Program

INTER-EXCELLENCE II

Veřejná soutěž

SMSM2026LU001

Hlavní účastníci

České vysoké učení technické v Praze / Fakulta informačních technologií

Druh soutěže

VS - Veřejná soutěž

Číslo smlouvy

MSMT-6303/2026-24

Název projektu anglicky

Computer-assisted mathematical proofs

Anotace anglicky

This project will create novel rigorous computer-assisted methods for a better understanding of large-scale networks. These networks can be seen in many real-life situations such as routing on the Internet, connections between users on social networks, or protein interactions inside a cell. Furthermore, large-scale networks form the foundation for addressing key challenges in pure mathematics and computer science. Our main aim is to develop new techniques of using a computer to prove new theorems in combinatorics, geometry, and number theory. These techniques will be used to attack some well-known open problems regarding graph colorings and partitioning (e.g. the conjecture of Erdős on making triangle-free graphs bipartite), lower and upper bounds on Ramsey numbers, hypergraph Turán problems (e.g. the respective Turán densities of K4- and C5-), the conjecture of Erdős-Szekeres on the existence of convex polygons in the plane, and bounding the number of monochromatic k-term arithmetic progressions in every coloring of a finite field. The tools that we intend to use to tackle these open problems will come from both mathematics and computer science: Szemerédi's regularity method, the hardcore and the Potts models, the Lovász local lemma and the entropy compression method are among the mathematical ones, those from computer science include SAT/SMT solvers, reinforcement learning, semidefinite and mixed-integer programming, and symbolic algebra systems.

Kategorie VaV

ZV - Základní výzkum

OECD FORD - hlavní obor

10101 - Pure mathematics

OECD FORD - vedlejší obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

OECD FORD - další vedlejší obor

—

CEP - odpovídající obory <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)

AF - Dokumentace, knihovnictví, práce s informacemi<br>BA - Obecná matematika<br>BC - Teorie a systémy řízení<br>BD - Teorie informace<br>IN - Informatika

Zahájení řešení

1. 3. 2026

Ukončení řešení

30. 6. 2029

Poslední stav řešení

Z - Začínající víceletý projekt

Poslední uvolnění podpory

—

Důvěrnost údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Systémové označení dodávky dat

CEP26-MSM-LU-R

Datum dodání záznamu

24. 4. 2026

Celkové uznané náklady

8 442 tis. Kč

Výše podpory ze státního rozpočtu

8 442 tis. Kč

Ostatní veřejné zdroje financování

0 tis. Kč

Neveřejné tuz. a zahr. zdroje finan.

0 tis. Kč