% This file:
%   http://anggtwu.net/LATEX/2025ebl-abs.tex.html
%   http://anggtwu.net/LATEX/2025ebl-abs.tex
%          (find-angg "LATEX/2025ebl-abs.tex")
% Author: Eduardo Ochs <eduardoochs@gmail.com>
%
% (defun c () (interactive) (find-sh "pdflatex 2025ebl-abs.tex"))
% (defun d () (interactive) (find-pdf-page    "2025ebl-abs.pdf"))
% (defun e () (interactive) (find-fline       "2025ebl-abs.tex"))
%
\documentclass[11pt]{article}

\usepackage[english]{babel}
%\usepackage[latin1]{inputenc} % for accents in Portuguese
\usepackage[utf8]{inputenc} % for accents in Portuguese using unicode

% ***PLEASE DO NOT MAKE CHANGES TO THE LINES BELOW***

\usepackage[centertags]{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{cite}
\usepackage{geometry}
\geometry{bottom=1.5cm,top=1.5cm,left=3cm,right=2cm}
\usepackage{indentfirst}

\date{}

%-------------------------- AUTHORS' PACKAGES ----------------------------%

% Place the packages used in your abstract here
% Examples:

%\usepackage{bussproofs}
%\usepackage{tikz}

%-------------------------- AUTHORS' MACROS -------------------------------%

% Place your macros here
% Examples:

%\newcommand{\C}{\ensuremath{\mathcal{C}}}
%\newcommand{\oid}{\ensuremath{\Leftrightline}}
%\newcommand{\fde}{$F\!D\!E$}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% DOCUMENT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

%------------------------------- TITLE -----------------------------------%

\title{Kind of proposal: Talk\\
      \textbf{Adapting Lean tutorials to the Brazilian case}
}

\author{
	{\large  \textsc{Eduardo Ochs}}\thanks{eduardoochs@gmail.com}\\
	{\small UFF, Rio das Ostras, RJ, Brazil} \\
}

\maketitle

%-------------------------------- KEYWORDS -----------------------------------%

\textbf{Keywords:} Proof Assistants, Lean

\vspace{1cm}

%-------------------------------- ABSTRACT ------------------------------------%

Lean4 (\cite{Overview}) is a proof assistant that is also a
general-purpose language, and that has ``metaprogramming facilities''
(\cite{Meta}) 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 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.



%------------------------------- REFERENCES -----------------------------------%

\begin{thebibliography}{00}

% Unpublished paper (How to cite: \cite{Weiss-2018})
\bibitem{Overview} {\em Lean Documentation Overview}. \\
  Available at {\tt https://lean-lang.org/lean4/doc/}.

\bibitem{Meta} {\em Metaprogramming in Lean4}. \\
  Avaiable at {\tt
    https://leanprover-community.github.io/lean4-metaprogramming-book/}.

\bibitem{Courses} {\em Courses using Lean}. \\
  Available at {\tt
    https://leanprover-community.github.io/teaching/courses.html}.

\bibitem{EmacsConf2024} {\em Emacs, eev, and Maxima -- Now!}. \\
  Avaiable at {\tt
    http://anggtwu.net/emacsconf2024.html}.

\bibitem{Oficina0} {\em Oficina de Lean4 -- versão 0}. \\
  Avaiable at {\tt
    http://anggtwu.net/2024-lean4-oficina-0.html}.


\end{thebibliography}

\end{document}