Formalisation is the process of digitalising mathematical results, teaching them to a computer. It has several benefits, the most obvious being the verification of the correctness of theorems beyond any reasonable doubt, starting from the axioms. Formalisation is becoming a more and more popular activity for mathematicians. The existence of huge libraries of formalised mathematics will have an important impact in the daily life of the working mathematician, who will soon be able to formalise their own research and have databases of theorems, rather than databases of papers. In the next few years, computer programs for formalization — called proof assistants — will also be able to help in mathematical research, taking care of “routine” calculations and similar problems. Many proof assistants can be used to formalise mathematics. Two of the most commonly used today by “standard mathematicians” are Lean and Coq, and the conference will mainly focus on the first. Lean comes with a vast library of formalised mathematics, mathlib. The existence of such a library allows one to work on contemporary mathematics. For example, one spectacular recent result has been the formalisation, by Commelin, Topaz and several other people, of one of the main results by Clausen and Scholze about condensed mathematics. This is cutting edge mathematics, using several theories, from functional analysis to homological algebra. The meeting’s main goal is to introduce mathematicians to Lean and to formalisation in general. There will be several talks, given by Lean experts, to explain the basics and provide examples, as well as many “practice sessions”, where participants will use Lean in real world situations. Taking advantage of the presence of many French scientists working in Coq, we also plan to invite some of them to offer three or four talks about this other proof assistant, mainly discussing differences, similarities and potential collaborations. The conference’s focus will at any rate be about formalising “standard mathematics”, and in particular it will neither be about foundations of mathematics nor programming. At the end of the week people will have drafts of results that can soon be included into mathlib, tangibly contributing to the development of formalised mathematics. We expect that the conference will enable people to start formalising modern mathematics, and their own research in the near future. Lean for the Curious Mathematician 2024 will be part of the series États de la Recherche SMF of the French Mathematical Society.