Quick
index
main
eev
eepitch
maths
angg
blogme
dednat6
littlelangs
PURO
(C2,C3,C4,
 λ,ES,
 GA,MD,
 Caepro,
 textos,
 Chapa 1)

emacs
lua
(la)tex
maxima
 qdraw
git
lean4
agda
forth
squeak
icon
tcl
tikz
fvwm
debian
irc
contact

Proceedings do EBL - pergunta sobre o tema do artigo (30/set/2025)

1. Eduardo
2. Bruno Lopes
3. Eduardo
4. Eduardo
5. Bruno Lopes
6. Eduardo
7. Eduardo
8. Bruno Lopes
9. Eduardo
10. Bruno Lopes
11. Eduardo
12. Bruno Lopes
13. Eduardo

O e-mail original está aqui: PDF.


1. Eduardo

Subj: Proceedings do EBL - pergunta sobre o tema do artigo
From: Eduardo Ochs
Date: 30 September 2025 at 12:57
To: Bruno Lopes

Oi Bruno! Tudo bem?

Eu fiz uma apresentação no EBL sobre dois assuntos muito conectados - tutoriais de Lean e de Maxima - mas no EBL o meu foco foi principalmente nos tutoriais de Lean... o abstract era este:

Lean4 is a proof assistant that is also a general-purpose language, and that has ``metaprogramming facilities'' that let people extend its syntax in many ways. It is becoming very popular, and the page \cite{Courses} has links to more than 40 courses on Lean, or using Lean.

{\sl I don't think that these courses are adequate for Brazilians.} They all start from some point like ``everybody knows VSCode'' and they move to non-trivial ideas very quickly. But ``everybody knows the programs such and such'' is not true in Brazil at all; half of the Brazilian logicians that I know only use computers in a very basic way, and here ``knowledge about programs does not propagate'' (see \cite{EmacsConf2024}).

In this presentation I will show how I adapted the approach in \cite{EmacsConf2024} -- that I use to teach Maxima to undergraduate students with {\sl very} little experience with computers -- to create a short workshop on Lean (\cite{Oficina0}) that teaches people how to install Lean4, how to navigate its manuals, how to understand its interface, and how to run and modify simplified versions of some examples from the main books on Lean.

Eu estou preparando um artigo pros proceedings do EBL que vai ser praticamente só sobre como eu tenho usado o Maxima com alunos sem base nenhuma, e que só vai mencionar o Lean bem brevemente - e o abstract vai ser totalmente diferente desse aí de cima, óbvio.

Vocês têm alguma regra sobre o quão próximo o artigo pros proceedings tem que ser do que a gente apresentou no congresso? Eu imagino que eu vá perder alguns pontos por mudar um pouco de assunto, mas que o artigo vai ser bom o suficiente pra compensar isso...

Grato de antemão =),
Eduardo


2. Bruno Lopes

From: Bruno Lopes
Date: 30 September 2025 at 13:10
To: Eduardo Ochs

Oi, Eduardo!

Pode haver crítica por parte do revisor, mas não há impedimento. Submeta!!!

Abraço,

Bruno.

[Quoted text hidden]


--
Bruno Lopes
Professor Adjunto
Instituto de Computação
Universidade Federal Fluminense
http://www.ic.uff.br/~bruno


3. Eduardo

From: Eduardo Ochs
Date: 30 September 2025 at 13:23
To: Bruno Lopes

Oba! Obrigado! =)
[[]], E.

[Quoted text hidden]


4. Eduardo

From: Eduardo Ochs
Date: 10 February 2026 at 19:04
To: Bruno Lopes

Brunoooo, socorro!

Eu tou quase submetendo o artigo pros proceedings to EBL mas as instruções que eu encontrei pra deixar ele "no formato certo" me pareceram simples demais... as que eu encontrei eram tipo "use espaço duplo e faça as coisas tais e tais com as figuras numeradas", e como as minhas figuras não são numeradas, são intercaladas com o texto, eu só precisei use \usepackage{setspace} e \doublespacing... isso é bem mais simples do que as dos outros artigos que eu já submeti, que exigiam umas documentclasses bugadas...

A deadline é hoje à meia noite?

Vou te mandar a versão atual do meu artigo só pra constar/por curiosidade, mas ainda tenho que reescrever o abstract, a última seção, e umas outras coisinhas...

[[]],
Eduardo

[Quoted text hidden]

Anexo: ochs_double_spaced_2026feb10_19:03.pdf
Anexo: ochs_single_spaced_2026feb10_19:00.pdf


5. Bruno Lopes

From: Bruno Lopes
Date: 10 February 2026 at 21:05
To: Eduardo Ochs

Oi, Eduardo!

Pode submeter assim. Não consigo verificar em detalhes, mas aquelas instruções foram copiadas do site. Ao que entendi, são vagas porque querem apenas facilitar a leitura do revisor. Eu tô com sono, então não vou ficar aguardando até meia-noite pra fechar o sistema :)

Mas não tenho como garantir que o pessoal do IGPL não o faça (eles exigem total acesso ao sistema).

Abraço,

Bruno.

[Quoted text hidden]


6. Eduardo

From: Eduardo Ochs
Date: 10 February 2026 at 21:42
To: Bruno Lopes

Obrigado!
Falta pouquinho aqui!
Boa noite! =) =) =)
E. =)

[Quoted text hidden]


7. Eduardo

From: Eduardo Ochs
Date: 11 February 2026 at 00:15
To: Bruno Lopes

Oi Bruno! Submeti, e já vi vários typos 😖😥😭... A gente tinha que te mandar algumas sugestões de pareceristas, né? Esse é o meu primeiro artigo sobre Educação Matemática e Computer Algebra, e eu só comecei a estudar essas coisas a sério há um ano atrás, então as sugestões que eu tenho são só essas daqui:

João Marcos ,
Wilhelm Alexander Cardoso Steinmetz ,
Yuriko Yamamoto Baldin ,
Márcia Fusaro Pinto

Todos os quatro são pessoas com as quais eu já conversei ao vivo, e a única pessoa que eu sei que conhece muitos dos itens da bibliografia é a Márcia Fusaro Pinto... acho que o melhor modo de arranjar pareceristas especialistas nos assuntos do artigo é falar com a Márcia Fusaro e pedir recomendações pra ela.

[[]], obrigado, etc =),
Eduardo

[Quoted text hidden]


8. Bruno Lopes

From: Bruno Lopes
Date: 11 February 2026 at 05:55
To: Eduardo Ochs

Oi, Eduardo!

Pode me enviar uma versão mais atual por aqui que deu ainda consigo substituir.

Por favor põe as sugestões de revisores como comentário na submissão.

Abraço,

Bruno

Bruno Lopes
Professor Adjunto
Instituto de Computação
Universidade Federal Fluminense
http://www.ic.uff.br/~bruno


9. Eduardo

From: Eduardo Ochs
Date: 11 February 2026 at 09:05
To: Bruno Lopes

Oi Bruno!

Eu tentei, mas o sistema só tá me deixando editar umas pouquinhas coisas, e essas pouquinhas não incluem os comentários... a não ser que tenha algum truque que eu não descobri...

Tou mandando em anexo uma versão do artigo com um montão de coisas consertadas!

[[]], E. ... =)

[Quoted text hidden]

Anexo: ochs_double_spaced_2026feb11_08:54.pdf 355K


10. Bruno Lopes

From: Bruno Lopes
Date: 11 February 2026 at 09:38
To: Eduardo Ochs

Já atualizei!

[Quoted text hidden]


11. Eduardo

From: Eduardo Ochs
Date: 11 February 2026 at 12:26
To: Bruno Lopes

Oi Bruno! Tudo bem?

Deixa eu te perguntar uma coisa - que deve ser óbvia pra quase todo mundo, mas eu moro no mato e não sei...

Qual é o status desse artigo antes dos referees sugerirem modificações e (espero!) ele ser aceito? Tipo: eu posso mandar ele pro pessoal da mailing list do Maxima que discutiu umas idéias dele comigo? Ou melhor: se eu for mandar pra essas pessoas é pra mandar só em privado, ou já posso mandar pra mailing list com os disclaimers adequados?

Grato de antemão e desculpa a jequice... =P,
Eduardo

[Quoted text hidden]


12. Bruno Lopes

From: Bruno Lopes
Date: 11 February 2026 at 12:29
To: Eduardo Ochs

Sugestão: põe um pre-print no arXiv.

Você pode mandar em privado, sem problemas. Mas as revistas costumam não implicar com o arXiv.

[Quoted text hidden]


13. Eduardo

From: Eduardo Ochs
Date: 11 February 2026 at 12:57
To: Bruno Lopes

BOAAA!
Obrigado! =)
E. =)

[Quoted text hidden]