=Paper=
{{Paper
|id=Vol-1785/fm4m
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1785/fm4m.pdf
|volume=Vol-1785
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-1785/fm4m.pdf</pdf>
<pre>
         FM4M 2016: Formal Mathematics for
                 Mathematicians
    FMM is a workshop affiliated with CICM 2016 intended to gather together
mathematicians interested in computer assistance and researchers in formal and
computer-understandable mathematics.
    The mathematical community today seeks various ways to support their work
by accessing digital libraries and repositories, applying Internet search techniques
to better explore and classify the vast mathematical knowledge, and to combine
computer calculations with informal mathematics. Related methods have been
developed a lot recently by the formal community, allowing the building of very
large formal mathematical libraries and full formal verification of large compu-
tationally involved proofs such as those of the Kepler conjecture and the Four
Color Theorem.
    It is very important to establish a platform for both communities to interact.
The successful development of computerized formal mathematics and its general
availability very much depends on the feedback that the formalized mathematics
developers can obtain from the community of working mathematicians. This
workshop’s main objective is to explore ways of building synergy between the
two communities.
    Over the last decades, we witnessed a number of successful instances of
computer-assisted formalization of mathematical problems. Research in this field
has been boosted by the development of systems for practical formalization of
mathematics (proof assistants), a creation of large repositories of computer-
verified formal mathematics, and integration of interactive and automated meth-
ods of theorem proving. Proof assistants provide a very useful teaching tool suit-
able for undergraduate instruction, in particular for training beginning students
in writing rigorous proofs. An expected wider outcome of this workshop is there-
fore setting up of an annual series of meetings between working mathematicians
and researchers in formal mathematics as well as graduate students with strong
background in these fields.

                                                     July 2016, Adam Naumowicz

</pre>