Videos for Sunday's paper, lecture 1 demo online, practical tips
|
To prepare Sunday's paper (Vaswani et al., Attention Is All You Need), it may be interesting to watch chapters 5 to 7 of 3Blue1Brown's Deep Learning series, which explain transformers, attention and the feed-forward layers visually and quite thoroughly: https://www.youtube.com/watch?v=wjZofJX0v4M&list=PLZHQObOWTQDNU6R1_67000Dx_ZCJB-3pi&index=6 The max-flow min-cut demo from lecture 1 is now online: https://github.com/joachimneu/demo-maxflowmincut If you're curious, have a look at the skills under .claude/skills. The git tag step06a-demo-4 is the broken mechanization, step06b-demo-4 the correct one. The repository may also be of interest from a practical, "tools" perspective: it shows how to put together the AI and Lean in a workspace. I use a similar setup for every research project and mechanization: a) Everything is in one git repository, which I open in VS Code. b) The repository contains a devcontainer: in effect a small Linux VM, which VS Code builds and opens automatically. It installs Lean and Claude Code, both as command-line tools (see .devcontainer/setup.sh) and as VS Code extensions (see .devcontainer/devcontainer.json). (OpenAI Codex etc. would work just as well, you just have to adjust the devcontainer accordingly.) c) The agent works only inside the container, so it cannot touch my system or other projects, and everything it changes is in git. This way it can run without permission checks, and install whatever tools it wants, e.g., for converting PDFs to Markdown for faster/cheaper processing. To run this yourself, install Docker, VS Code with the Dev Containers extension, and git. Everything else is installed automatically inside the container. Clone the repository, open it in VS Code, choose "Reopen in Container", and look around. If you get stuck, post on Piazza (https://piazza.com/technion.ac.il/fall2026/2360802 ) or ask your agent. :) |
| פורסם ב-4/11/2026, 22:56:40 Created on 4/11/2026, 22:56:40 Создано4/11/2026, 22:56:40 تم النشر ب-4/11/2026, 22:56:40 |
Lecture 1 slides, paper assignment, roles for 8 Nov
|
The slides of lecture 1 are uploaded on Webcourse. Please make sure you have completed all three of the following sign-up steps: a) Enroll on GR++/Webcourse (so you get announcements and materials). b) Enroll on the SAP Portal (so you can get a grade). c) Fill out the sign-up form (so I know a bit about your background and interests to tailor the class): https://forms.gle/j9pDiYX1psmMUaKi8 If you have not yet picked the paper you will present, please sign up in the sheet: https://docs.google.com/spreadsheets/d/1Ry2EHe4YOMsxHD8frxlwSV59zaSPYx4iSNyyq9TTr5w/edit?usp=sharing . If no slots are left, please contact me. The current paper assignment and the roles for next week are posted on Webcourse, in the "Paper Assignment" section of the course overview. If you present in week 3 (15 Nov), please contact me to find a time to meet and discuss your storyboard and your slides. Have fun with Tao's Machine-Assisted Proof (article: https://doi.org/10.1090/noti3041 , video: https://www.youtube.com/watch?v=5ZIIGLiQWNM ) and with the Lean games (https://adam.math.hhu.de/ )! A screenshot of one finished game is due before class on 29 Nov, 10:00 Israel time. If you have any questions, please contact me. |
| פורסם ב-2/11/2026, 11:31:03 Created on 2/11/2026, 11:31:03 Создано2/11/2026, 11:31:03 تم النشر ب-2/11/2026, 11:31:03 |
Action required: complete all three sign-up steps
|
To participate in the seminar, please make sure you have completed all three of the following steps: a) Enroll on GR++/Webcourse. b) Enroll on the SAP Portal. c) Fill out the sign-up form: https://forms.gle/j9pDiYX1psmMUaKi8 If you run into any difficulty with these steps (e.g., no seats left, enrollment cap, waitlist, etc), please contact the instructor. |
| פורסם ב-29/10/2026, 12:23:29 Created on 29/10/2026, 12:23:29 Создано29/10/2026, 12:23:29 تم النشر ب-29/10/2026, 12:23:29 |