https://messenger.abeto.co/

Cute browser game with a pretty distinct art style.

https://arstechnica.com/science/2025/09/meet-the-2025-ig-nobel-prize-winners/

Let's celebrate the victory march of Science!

https://www.youtube.com/watch?v=PnQ0eQrKF4g

Curious how our activities exert evolutionary pressure over various animal species, which gets recorded into their genes. Well, any activity on the planet exerts evolutionary pressure, that's the whole point. But humans act on unprecedentedly short time scales, and the nature notices (and adapts).

https://www.answer.ai/posts/2025-06-05-readbench.html

The folks designed and implemented the ReadBench benchmark for testing Vision-Language Models (VLMs) and other Multimodal LLMs essentially on the OCR tasks.

The results are kinda as expected, but still show that you can't simply pile all of your scanned documents into a DB and expect a VLM to efficiently sift through them all and extract necessary information.

https://julialang.org/blog/2025/10/julia-1.12-highlights/

Julia 1.12 is out. This one largely continues the long-standing theme of improvements to compilation and packaging.

Compilation improvements include the option to build the Julia itself with LLVM BOLT (as well as LTO and PGO), and precompilation times tracing.

For building self-contained binary images there's now an expreimental option to --trim all statically unreachable code, which yields way smaller binaries, but (expectedly) breaks on dynamic dispatches and other dynamic features. Looks very similar to AOT compilation for Java and C# which also breaks on reflection and similar dynamic features.

Other packaging improvements include support for workspaces comprising several closely related projects (like a library + tests + benchmarks + docs + examples) and dedicated (CLI) apps.

"Не имбирь мне мозги!"

This year’s London Mathematical Society (LMS) / British Computer Society -- Formal Aspects of Computing Science (BCS-FACS) Evening Seminar will feature Jeremy Avigad as the distinguished speaker. Registration is free but required in advance.

https://www.lms.ac.uk/events/lms-bcs-facs-seminar-jeremy-avigad

Date: 6 November 2025
Time: 19:00 (UK time)
Format: Online via Zoom
Talk title: Mathematics in the Age of AI
Abstract:
New technologies for reasoning and discovery are bound to have a profound effect on mathematical practice. Proof assistants are already changing the nature of collaboration, communication, and curation of mathematical knowledge. Automated reasoning tools are used to find mathematical objects with specified properties or rule out their existence, and to decide or verify mathematical claims. Machine learning and neural methods can discover patterns in mathematical data, explore complex mathematical spaces, and generate mathematical objects of interest. Neurosymbolic theorem provers, now capable of solving the most challenging competition problems, combine aspects of all of these technologies.

It is helpful to keep in mind that the phrase "AI for mathematics" encompasses several distinct technologies that overlap and interact in interesting ways. In this talk, I will survey the landscape, describe a few landmark applications to mathematics, and encourage you to join me in thinking about how mathematicians and computer scientists can collaborate to guide mathematics through this era of technological change.

The talk shall be uploaded to YouTube as well as the previous ones:
https://www.youtube.com/channel/UCvp7jsbXjx2k8sGEkdtWCAw

To whom it might concern. There's the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM):
https://popl26.sigplan.org/series/pepm

There's still some time to send a paper to the 2026 instance.

The Computing Science division at the University of Gothenburg has a 360 days research position to work with Prof. Thierry Coquand and his group.
Deadline for application is Oct 30th.

The project is about the study of dependent type theory extended with univalence with applications to synthetic mathematics. Prime examples are synthetic algebraic geometry and synthetic Stone duality, but it might be other kind of synthetic mathematics, such as study of higher categories.

https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=38480

PhD is required. 😏

A Summer School in December! Welcome to Australia:

https://comp.anu.edu.au/lss/

This year the focus is on Modal Logics and Type Theories, and software verification in Isabelle/HOL.

https://www.youtube.com/watch?v=NUYNby4MJms

Leatherman Wave with a MagnaCut blade!!! Fuck me!

They formalized (and mechanized) the https://en.wikipedia.org/wiki/Z_notation in Isabelle/HOL:
https://www.isa-afp.org//entries/Z_Toolkit.html

Finally a decent IDE and proof automation for Z. 😏

https://trop.in/blog/i-have-to-live-in-a-forest-to-work-on-open-source

It doesn't cover all the details and nuances, but still. That's how life happens to some of us.

https://www.laser-foundation.org/verifai-26/

The VERIFAI workshop, the first of its kind, is devoted to the interplay between the two technologies: not only how to verify AI tools but also (the main focus) how verification techniques can make “vibe coding” efficient and reliable.

20 December 2025: submission deadline for full papers (max 15 pages) or extended abstracts (2 to 5 pages) for participation in the workshop.

8-11 March 2026: workshop

https://www.bbc.co.uk/mediacentre/2025/new-ebu-research-ai-assistants-news-content

AI assistants misrepresent news

That's not surprising news at all. But I didn't read the actual report yet, and there might be many "threats to validity". In particular, I'd like to see more LLMs tested, at least Anthropic, xAI, Qwen, and DeepSeek, but alas...

https://dmkpress.com/catalog/computer/freeware/978-5-93700-419-2/

Для разнообразия — вводная книжка про QGIS от ДМК Пресс.

Как хобби-пользователь QGIS, не обременённый профильным картографическим образованием, могу сказать, что QGIS — это монстр. Огромный универсальный пакет, который может всё. К сожалению, обратная сторона его мощи и универсальности — огромное количество функций и концепций, из которых я знаю, может быть, 1%.

В результате, посредством крайне выборочного чтения документации, ответов с GIS Stack Exchange, тьюториалов и LLMs, я сумел худо-бедно настроить пару проектов, которые выдают приемлемые для моих целей карты. Но шаг влево, шаг вправо — и я полностью потерян, не понимаю, что происходит или не происходит, как исправить и что вообще делать.

Кажется, что такая вот недлинная (300 страниц) и недорогая книжечка как раз способна обрисовать достаточно "общей картины" чтобы понимать, что и как делать в основных ситуациях и хоть какие термины гуглить, если нужно что-то нетривиальное. Для начала она знакомит с основными типами (тематических) карт, для каких целей они используются и каким принципам должны следовать чтобы результат был внятным и читаемым.

Во второй части книга объясняет как добиваться тех или иных результатов конкретно в QGIS, потому что это редко бывает очевидным. Из-за высокой гибкости часто страдает удобство выполнения простых действий. Поэтому QGIS далёк от "интуитивно понятного", и подробные пошаговые руководства сильно помогают.

Tomorrow, Friday, 24

https://events.iu.edu/event/2087515-big-proof-formal-proof-from-a-collaborative-lens

Big Proof: Formal Proof from a Collaborative Lens

https://tdejong.com/mhe60/
Types and Topology
A workshop in honour of Martín Escardó's 60th birthday
17–18 December 2025

Attendance is free, but registration closes 21 November 2025
There will be a Zoom livestream.