In addition to the Church of the Least Fixed Point I propose "β-reduction Witnesses".

Serendipitously stumbled upon https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/ and it's kinda curious to revisit the answers from 7 years ago.

The most obvious is that Univalent Mathematics indeed grew to dominate research at least in Foundations of Mathematics and Type Theory.

Second, I don't think we can say mechanized proofs are widespread (though that's pretty vague) but I bet the panellists would be surprized how far they penetrated already. And we still have 28 years to go which seems like a lot considering the rate of the spread.

“One doesn’t read a mathematical paper, what one gets is the idea to reconstruct the argument it’s not that people (generally speaking) would be …checking the logic line by line — they would go and extract the fundamental idea; that’s really the essential thing.”

I would say exactly the same about mechanized proofs. For one thing you don't even need to check the proof line-by-line, a machine already did that. Second, I'm huge fan of structured proofs exactly because they show you the shape of the argument and help extracting the major ideas and relationships behind it.

Near the end the author raises concerns of a technological lock-in into a particular system. With the current state of affairs and pretty "heated competition" among different systems that seems unlikely. Especially noting that in reality the systems not that much compete with one another as occupy different "ecological niches" and specialize for different areas and styles of work. Which addresses the last concern of the author, that mathematicians will have to adapt to a system designed for proving software correct and not mathematics. I have an impression that many proof assistants kinda "abandon" their "software correctness roots" for the glory of concurring Pure Math. 😁

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

WOW! That sounds HUGE! Extremely ambitious and exciting. Many right words, a number of unobvious insights. I wish them great success.

https://press.princeton.edu/books/paperback/9780691145990/how-mathematicians-think

"How Mathematicians Think: Using Ambiguity, Contradiction, and Paradox to Create Mathematics"

Sounds like serious fun! 😁

https://arxiv.org/pdf/2112.02142.pdf
An Impossible Asylum
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki

In 1982, Raymond Smullyan published an article, “The Asylum of Doctor Tarr and Professor Fether,” that consists of a series of puzzles. These were later reprinted in the anthology The Lady or The Tiger? and Other Logic Puzzles. The last puzzle, which describes the asylum alluded to in the title, was designed to be especially difficult. With the help of automated reasoning, we show that the puzzle’s hypotheses are, in fact, inconsistent, which is to say, no such asylum can possibly exist.

Exposing mad scientists with the help of the Vampire! 🧛😁

By the way someone fixed something and Google Meet seems to work fine in Firefox again. I mean backgrounds and effects still don't but at least the main functionality works as before.

Ну и некоторая "выжимка" из этих приёмов визуализации была — снова значительное время назад — опубликована в блоге Stack Overflow: https://stackoverflow.blog/2022/03/03/stop-aggregating-away-the-signal-in-your-data/

#datascience #analysis #visualization

It was recommended to me, the book "Introduction to Statistical Learning":
https://hastie.su.domains/ISLR2/
and the lectures based on it:
https://www.youtube.com/watch?v=5N9V07EIfIg&list=PLOg0ngHtcqbPTlZzRHA2ocQZqB1D_qZ5V

The lectures seem pretty fun. 😊
#statistics #datascience #book #lectures

https://percival.ink/

It's essentially ObservableHQ, but with Datalog instead of JS while reusing the same plotting libraries. Genius.

#datascience #visualization #notebook

ADnD — Advanced Development and Delivery! 😂

DDnD — Development, Deployment and Delivery.

https://www.inkandswitch.com/crosscut/

Очень крутая попытка сделать визуальное программирование в смысле визуального моделирования, а не очередной неуклюжий GUI для представления графа потока данных и абстрактных функций. Поэтому Crosscut работает на основе непосредственной манипуляции конкретными объектами. Конечно, наглядно-образное мышление супротив абстрактного работает только до определённого предела, но при наличии компьютерной поддержки этот предел отодвигается удивительно далеко. Обратите внимание на "bidirectional evaluation".

Кот выкатил тяжёлую ортиллерию.

https://cryochamber.bandcamp.com/album/mothership
Pretty cool Vangelis' Blade Runner vibes. 😁

Судя по https://algorithmsbook.com/#outline — очень крутая книга.
#machinelearning #reinforcementlearning #multiagent #uncertainty #optimization #julia

https://www.cut-the-knot.org/proofs/Uncountability.shtml

A proof of uncountability of Reals for those who don't like Diagonal Argument but like Games. 😁

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

Yay, they've uploaded the recording! A fascinating but puzzling topic. Bayesian priors update is not as simple as LessWrong fans make it sound. 😁

#probability #bayes

Степень прожарки проекта:
- норм
- медиум-норм
- норм с кровью

https://www.trymito.io/

Every Data Analysis platform attempts to expand until it includes a Spreadsheet. Those platforms which cannot so expand are replaced by ones which can.

Or maybe

Any sufficiently complicated Data Analysis platform contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Excel.

(Paraphrasing https://en.wikipedia.org/wiki/Jamie_Zawinski#Zawinski's_Law and https://en.wikipedia.org/wiki/Greenspun%27s_tenth_rule if you didn't recognize them at once. 😊)

Though curious thing about this tool is that it generates Python code that performs transformations you specify in the spreadsheet. Advantages are obvious. Would be super cool if it could synchronize the other way round, but it can't unfortunately.

#datascience #jupyter #python

In other news. Lawrence Paulson started a series of introductory posts to Isabelle/HOL: https://lawrencecpaulson.github.io/2022/05/04/baby-examples.html

WOW this is mind-blowing: http://liamoc.net/holbert/
A browser-based notebook-style theorem prover for higher-order logics. Aimed at educational applications, and as such can switch between more formal tree-like and a book-style natural deduction proofs presentation.

Here's a notebook about MLTT: http://liamoc.net/holbert/?https://gist.githubusercontent.com/brendanzab/1b4732179b15201bf33fed6dbca02458/raw/mltt.holbert