[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-23 09:57, Louis Garde wrote:
> Le 22/08/2020 à 20:39, mechvel at scico.botik.ru a écrit :
>> I tried to demonstrate that people who pay attention to restrict EM in 
>> mathematics always
>> rely on this "unsafe" proof tool in their life.

> A proof is defined only within a formal system, defined by a fixed set
> of rules and axioms, whereas my life (and yours) is not governed by a
> fixed set of rules and axioms: intuitions from the real life are
> sometimes usefull, sometimes misleading !

A proof is a philosophical notion, it is not necessarily formal.
And logic is first and initially philosophical, and then, may be, 
mathematical.
For example, coroners and advocates also deal with proofs, only not so 
rigorous.
Even in mathematics most proofs are not formal.
Otherwise mathematicians would not be able to solve anything important.
They are formal only in Agda programs and in such systems.
In my letters I wrote about certain relation between logic in life and 
formal logic,
as it was, say, in the example with the lottery. There is a certain 
intuitive connection
between them.

--
SM