Why Mathematical Proof Is a Social Compact

[Ruy Jose Guerra Barretto de Queiroz]

Why Mathematical Proof Is a Social Compact

Number theorist Andrew Granville on what mathematics really is — and why objectivity is never quite within reach.

[Joao Marcos]

computadores podem nos ajudar a encontrar demonstrações, e não apenas verificá-las?

https://youtu.be/3l1RMiGeTfU?si=SL_Fi0q6q5T-y_33

bônus: código L∃∀N

outro bônus: história de crime em quadrinhos sobre matemática

JM

On Fri, Sep 1, 2023 at 9:06 AM Ruy Jose Guerra Barretto de Queiroz <r...@cin.ufpe.br> wrote:

Why Mathematical Proof Is a Social Compact

Number theorist Andrew Granville on what mathematics really is — and why objectivity is never quite within reach.

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
Você recebeu essa mensagem porque está inscrito 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 logica-l+u...@dimap.ufrn.br.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANSQ7QiAMi%2B8Yu3veAKWL_%2BqwYQ1A4-p0pBC9h-%2BvxBQqqtkGg%40mail.gmail.com.

--

http://sequiturquodlibet.googlepages.com/

[Joao Marcos]

computadores podem nos ajudar a encontrar demonstrações, e não apenas verificá-las?

https://youtu.be/3l1RMiGeTfU?si=SL_Fi0q6q5T-y_33

bônus: código L∃∀N

Também relacionado:

Can LLMs Generate Mathematical Proofs that can be Rigorously Checked? 

Meet LeanDojo: An Open-Source AI Playground With Toolkits, Benchmarks, and Models for Large Language Models to Prove Formal Theorems in the Lean Proof Assistant

https://www.marktechpost.com/2023/07/01/can-llms-generate-mathematical-proofs-that-can-be-rigorously-checked-meet-leandojo-an-open-source-ai-playground-with-toolkits-benchmarks-and-models-for-large-language-models-to-prove-formal-theore/ 

JM

--

http://sequiturquodlibet.googlepages.com/