https://xenaproject.wordpress.com/2020/04/30/the-invisible-map/
"The basic idea: our code will correspond to mathematical definitions and proofs, and our code will compile if and only if our proofs are correct. Such systems do exist — but in this post, we will just imagine what this kind of code might look like, and how easy it would be for a mathematician to write it. The “de Bruijn factor” of a system like this is the ratio (size of program which proves a theorem in our system) / (size of LaTeX file which proves the same theorem), and ideally this number should be small." JM -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LhBg-XHGVpqsbj3SPSfawcNrck3Sr0Y318K1NoaN7bUbQ%40mail.gmail.com.
