#	Pagina
attuale pagina	/open-h2020/projects/196037/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 1 - KaMCAM (Kac-Moody groups and Computer Assistants in Mathematics)

Teaser

Summary

The project addresses two distinct, yet interconnected work packages.
1) Curtis-Tits groups

This work package falls within the realm of algebra, more precisely group theory. This is broadly speaking the study of symmetry of certain geometric and combinatorial objects. Curtis-Tits groups are generalizations of a class of groups of relevance to Theoretical Physics called Kac-Moody groups. Generally such groups are in some sense infinite dimensional.
The purpose of the project is to completely classify and describe these groups In terms of a compact finite set of data and to study these groups and related geometric and combinatorial structures in terms of this data.
We also wish to explore applications in various areas of mathematics and computer science.

2) Mathematical Research and Teaching with Proof Assistants
The purpose of this work package was to address the well-known difficulties that students encounter when learning to write structured proofs, i.e. rigorous explanations of mathematical ore more generally formal logical statements.
There exist many useful software packages for teaching and assessing computational aspects of mathematics. However, one of the major obstacles in teaching conceptual understanding and critical thinking skills within mathematics and sciences in general the fact that it is hard to produce and assess sufficient numbers of practice problems.
There are so-called proof assistants, but these have been developed mainly for advanced computer science purposes and are unsuitable for students without advanced understanding of modern programming languages.
Notably in the current computer age, computational skills are increasingly becoming irrelevant, whereas transferable skills coming from conceptual understanding are increasingly important.

Work performed

\"The project addresses two distinct, yet interconnected work packages.
1) Curtis-Tits groups
We have been able to completely classify and describe these groups In terms of a compact finite set of data.
As a result of this classification we have discovered the existence of a large number of previously unknown groups. In order to show the existence of these groups we have also constructed a class of geometric combinatorial objects generalizing what are known as \"\"buildings\"\".
The methods that we have developed allowed us to obtain many algebraic and geometric properties of these groups and related finite groups.
Interestingly our classification methods have also been applied towards the revision of the famous classification of finite simple groups.

2) Mathematical Research and Teaching with Proof Assistants
We have more than achieved our goals and have developed a new software package which allows students to write proofs in natural language, have it verified by the powerful proof assistant Coq and automatically assessed, and have the resulting proof typeset using the professional typesetting system LaTeX used by scientists all over the world.
This has been piloted with student interns and plans are in place for a wider study with pre-university students.
We have started writing a companion textbook to be published by Springer Verlag. We have developed strong research connections with the theoretical computer science community working on proof assistants.\"

Final results

All results are by the very nature of mathematics beyond the state of the art. In fact some of our results are beyond our own expectations at the beginning of the project.

Whereas we have achieved most if not all result described in the project, not all of these have been published. However, we expect several more manuscripts to be submitted in the near future.
The development of the software package is ongoing as are plans for large scale dissemination and impact studies.