Zulip Chat Archive

Stream: maths

Topic: (partial) spanish translation of formalizing mathematics


Andrés Goens (Feb 21 2022 at 12:12):

#English

Hi!

Not sure if this is the place to post this. I gave a mini-workshop at the University of El Salvador (online) about Lean for mathematicians. Here's the link: https://github.com/goens/smf-ues-2022

For that I translated some of @Kevin Buzzard's Formalising Mathematics (2021) course and some parts of the Natural number game. I'm not sure on how to best give attribution according to the Apache license, I hope the text at the beginning referring to the text is okay? (please do let me know if not and I'll change it as necessary!)

There's going to be recordings also, in the Facebook site of the school of mathematics.


Español

Hola!

No estoy seguro si este es el lugar para postear esto. Di un minicurso en la Universidad de El Salvador (en línea) acerca del uso de Lean para matemáticos. Aquí está el enlace: https://github.com/goens/smf-ues-2022

Lo hice traduciendo partes del curso Formalising Mathematics (2021) de
@Kevin Buzzard y partes del Natural number game.

También va a haber una grabación del minicurso, hasta adonde entiendo en la página de Facebook de la escuela de matemáticas.

Chris Birkbeck (Feb 21 2022 at 13:11):

Que chévere! ¿Cuanto has traducido del juego de los números naturales? Si hay por lo menos algunos niveles sería bueno hacer una página donde se pueda jugar sin tener que instalar lean.

Chris Birkbeck (Feb 21 2022 at 13:13):

Por lo que me a dicho Kevin, no es tan difícil convertir los niveles a una página web

Andrés Goens (Feb 21 2022 at 13:54):

la parte del juego de lo números naturales fue una "traducción" un poco más liberal (tomando sólo partes, etc), sólo cubrí las propiedades de la suma y un poco de multiplicación

Andrés Goens (Feb 21 2022 at 13:56):

pero la verdad me gustó, podríamos hacer una traducción más completa, hay un ejemplo de alguien que lo hizo al coreano


Last updated: Dec 20 2023 at 11:08 UTC