Mastodawn

Reseña de «A new paradigm for mathematical proof?». https://jaalonso.github.io/vestigium/posts/2025/11/08-a-new-paradigm-for-mathematical-proof/ #Math #ITP #LeanProver #Agda

Reseña de «A new paradigm for mathematical proof?»

En la conferencia «A new paradigm for mathematical proof?», Emily Riehl explora los desafíos actuales en la verificación de demostraciones matemáticas. Ejemplos como la conjetura de Kepler y el progra

Vestigium

amen zwa, esq.Mar 28

I am aghast to discover that “coding camp” type publications on proof assistants, like #Agda and #Lean, do exist, complete with the all-too-common modern #IT anthem, “No need to know any mathematics”, emblazoned across the introduction, and subsequent pages littered with code samples, without proofs.

There are two primary uses of a proof assistant: to do mathematics and to write verified programmes. Both uses are built upon writing formal proofs. Without writing proofs, a proof assistant is almost an inconvenient, inefficient #programming language.

Boyd Stephen Smith Jr.Mar 27

RE: https://hachyderm.io/@BoydStephenSmithJr/116298200584577447

Anyone out there with some opinions on both @codeberg and @gitlab particularly for developing #Haskell, #Idris, #Lean, or #Agda ? If you can,, please address my concerns in the quoted toot.

Fraser Tweedale Mar 26

RE: https://functional.cafe/@hackuador/116282882755691464

Two more sleeps until the first #BFPG Hack Day of 2026! See yas there, curious minds!

#FP #Haskell #OCaml #Idris #Gleam #Lean #Scala #Erlang #Elixir #FSharp #Clojure #Lisp #Agda #Rocq #Rust #Scheme #Racket

Achim D. Brucker Mar 19

Want to learn more about the latest developments on using AI and (interactive) theorem proving in Mathematics? Wait no longer!

We have a great line-up of speakers at our online Workshop on AI and Theorem Provers in Mathematics. The workshop will be held online from 8th to 10th of April and attendance is free (registration required). For more details, visit the workshop website: https://aitpm.github.io/

#math #itp #theoremProving #isabelleHOL #lean #llm #ai #formal_mehods #agda #hol #mathematics

Workshop on AI and Theorem Provers in Mathematics (AITPM)

Workshop on AI and Theorem Provers in Mathematics

AITPM

Fraser Tweedale Mar 18

Thanks to Sirius-beta Labs who are once again sponsoring lunch for #BFPG Hack Day. UQ St Lucia, Saturday 28 March. Be there or be a lambda cube!

#FP #Haskell #OCaml #Idris #Gleam #Lean #Scala #Erlang #Elixir #FSharp #Clojure #Lisp #Agda #Rocq #Rust #Scheme #Racket

https://luma.com/uu28az9h

BFPG Hack Day - March 2026 · Luma

Come to BFPG Hack Day for some wholesome fun hacking on side projects, tackling tutorials, grinding axes and shaving yaks! Work together or independently.…

José A. Alonso Mar 15

Readings shared March 14, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/15-readings_shared_02-14-26 #AI #Agda #ITP #LeanProver #Math #Mizar

Readings shared March 14, 2026

The readings shared in Bluesky on 14 March 2026 are: From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. #LeanProver #ITP A formalization of Borel determin

Vestigium

José A. Alonso Mar 14

A formalization of abstract rewriting in Agda. ~ Sam Arkle, Andrew Polonsky. https://arxiv.org/abs/2603.10936v1 #Agda

A Formalization of Abstract Rewriting in Agda

We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate the relationships between them and their classical counterparts. We identify, and eliminate where possible, the use of classical logic in the proofs of standard ARS results. Our analysis leads to refinements and mild generalizations of classical termination and confluence criteria. We investigate logical relationships between several notions of termination, arising from different formulations of the concept of a well-founded relation. We illustrate general applicability of our ARS development with an example formalization of the lambda calculus.

arXiv.org

HoldMyType Mar 8

#Emacs uses the Unicode Character Database (UCD) compiled into its binary. Every codepoint has properties — category, bidirectional class, case folding, combining class, etc. Emacs loads this at startup and uses it for rendering, input methods, and font selection. Agda goes further — it uses the UCD to determine which codepoints are valid identifiers, operators, or whitespace, since #Agda allows Unicode operators like ∀ → ⊢ λ directly in source.
Fontconfig then maps codepoints to glyphs via font lookup. If no font covers the codepoint you get a replacement box.
#GraphQL OTOH has no native binary or raw-text type — everything is a JSON string, so any unescaped byte that's invalid in JSON (control chars, malformed UTF-8 sequences like your 0xD6 case) breaks the entire response. Emacs and Agda never have this problem because they read bytes directly and interpret encoding explicitly — they don't depend on an intermediate serialization format like JSON that has strict validity rule

Linotype Pilgrim Mar 5

Core #Agda language maintainer punts LLM slop from the project: "As a human being, you should also reject LLM salespeople, and the garbage they dump in our repository, for a variety of social reasons, including basic decency. …It is no coincidence that the logo of every LLM company is a butthole."