Computer-aided proofs and combinatorial exploration.

Instructors: Pascal Ochem and Michael Rao.

Prerequisites: Working knowledge in a computer language. Basic notions in complexity theory, algorithms, linear optimization.

Evaluation: Project.

Summary: The computer is used more and more often to help demonstrate mathematical theorems. We will introduce the subject by speaking about the history and proof of the 4-color theorem, first big theorem demonstrated with the help of the computer, and reflecting rather well the advantages and problems of this kind of approach. We will present classic classic tools for combinatorial explorations: reduction to a SAT problem or a linear program, backtracking, transfert matrix method, dynamic programming... An important part will be reserved for practical work.

Tentative outline:

• How a computer can help in mathematics or computer science ?
• Presentation of the history of some computer aided theorems in discrete mathematics, to learn advantages and disadvantages of such approcahes
• Presentation of classic tools for exploring combinatorial: reduction to a SAT problem or a linear program, backtracking, transfert matrix methods, dynamic programming...
• Concrete examples of different approaches to accelerate explorations: reduction of the search space, heuristics, and methodologies to speed up code.
• Practise !