MastodonTech.de

José A. AlonsoClarifying before reasoning: A Coq prover with structural context. ~ Yanzhen Lu et als. <a href="https://arxiv.org/abs/2507.02541v1" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2507.02541v1</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#CoqProver</a>

José A. AlonsoComputer-assisted proofs for differential equations and dynamical systems. ~ Maxime Breden. <a href="https://hal.science/tel-05142432/document" rel="nofollow noopener" translate="no" target="_blank">https://hal.science/tel-05142432/document</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoBourbaki: Self-generated and goal-conditioned MDPs for theorem proving. ~ Matthieu Zimmer et als. <a href="https://arxiv.org/abs/2507.02726v1" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2507.02726v1</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a>

José A. AlonsoThe φ-weighted recognition hamiltonian: A self-adjoint operator unifying automorphic L-functions, E 8 symmetry, and cosmic dynamics. <a href="https://www.researchgate.net/publication/393400892_The_ph-Weighted_Recognition_Hamiltonian_A_Self-Adjoint_Operator_Unifying_Automorphic_L-Functions_E_8_Symmetry_and_Cosmic_Dynamics" rel="nofollow noopener" translate="no" target="_blank">https://www.researchgate.net/publication/393400892_The_ph-Weighted_Recognition_Hamiltonian_A_Self-Adjoint_Operator_Unifying_Automorphic_L-Functions_E_8_Symmetry_and_Cosmic_Dynamics</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a>

José A. AlonsoRobust, end-to-end correctness proofs of industrial divide and square root RTL designs. ~ Sol Swords, Cuong Chau. <a href="https://www.arith2025.org/proceedings/215900a149.pdf" rel="nofollow noopener" translate="no" target="_blank">https://www.arith2025.org/proceedings/215900a149.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a>

José A. AlonsoComputational p-adics (in Isabelle/HOL). ~ Jeremy Sylvestre. <a href="https://www.isa-afp.org/entries/Computational_pAdics.html" rel="nofollow noopener" translate="no" target="_blank">https://www.isa-afp.org/entries/Computational_pAdics.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoParikh's theorem (in Isabelle/HOL). ~ Fabian Lehr. <a href="https://www.isa-afp.org/entries/Parikh.html" rel="nofollow noopener" translate="no" target="_blank">https://www.isa-afp.org/entries/Parikh.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a>

José A. AlonsoKraus maps (in Isabelle/HOL). ~ Dominique Unruh. <a href="https://www.isa-afp.org/entries/Kraus_Maps.html" rel="nofollow noopener" translate="no" target="_blank">https://www.isa-afp.org/entries/Kraus_Maps.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a>

José A. AlonsoThe oneway to hiding theorem (in Isabelle/HOL). ~ Katharina Kreuzer, Dominique Unruh. <a href="https://www.isa-afp.org/entries/Oneway2Hiding.html" rel="nofollow noopener" translate="no" target="_blank">https://www.isa-afp.org/entries/Oneway2Hiding.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a>

José A. AlonsoDoing Lean dirty: Lean as a Jupyter notebook replacement. ~ Philip Zucker. <a href="https://www.philipzucker.com/dirty_lean/" rel="nofollow noopener" translate="no" target="_blank">https://www.philipzucker.com/dirty_lean/</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a>

José A. AlonsoFormalising the local compactness of the adele ring. ~ Salvatore Mercuri. <a href="https://arxiv.org/abs/2405.19270" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2405.19270</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoReadings shared July 7, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/08-readings_shared_07-07-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/07/08-readings_shared_07-07-25</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Maxima" class="mention hashtag" rel="nofollow noopener" target="_blank">#Maxima</a>

José A. AlonsoLean: a theorem prover and programming language that enables correct, maintainable, and formally verified code. <a href="https://lean-lang.org" rel="nofollow noopener" translate="no" target="_blank">https://lean-lang.org</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a>

José A. AlonsoReadings shared July 5, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/06-readings_shared_07-05-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/07/06-readings_shared_07-05-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#CoqProver</a> <a href="https://mathstodon.xyz/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalMethods</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Maxima" class="mention hashtag" rel="nofollow noopener" target="_blank">#Maxima</a> <a href="https://mathstodon.xyz/tags/PVS" class="mention hashtag" rel="nofollow noopener" target="_blank">#PVS</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a>

José A. AlonsoThe filter game (in Lean 4). ~ Kevin Buzzard. <a href="https://adam.math.hhu.de/#/g/kbuzzard/FilterGame" rel="nofollow noopener" translate="no" target="_blank">https://adam.math.hhu.de/#/g/kbuzzard/FilterGame</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoA proof-assisted conversion of signal temporal logic formulas into negative normal form. ~ Danil Berrah, François Pessaux, Alexandre Chapoutot. <a href="https://hal.science/hal-05133722/document" rel="nofollow noopener" translate="no" target="_blank">https://hal.science/hal-05133722/document</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a>

José A. AlonsoFunctorial flattening of the state monad via vector‐space projection (A formally verified collapse model in Lean 4). ~ Jinu Jang. <a href="https://kairose-master.github.io/mu_eq_pi/pdf/mu_eq_pi.pdf" rel="nofollow noopener" translate="no" target="_blank">https://kairose-master.github.io/mu_eq_pi/pdf/mu_eq_pi.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a>

José A. AlonsoFormal methods at NASA: Past, present, and future. ~ Paul Miner, Natasha Neogi. <a href="https://ntrs.nasa.gov/api/citations/20250006044/downloads/NFM_Keynote_STRIVES-psm.pdf" rel="nofollow noopener" translate="no" target="_blank">https://ntrs.nasa.gov/api/citations/20250006044/downloads/NFM_Keynote_STRIVES-psm.pdf</a> <a href="https://mathstodon.xyz/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalMethods</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/PVS" class="mention hashtag" rel="nofollow noopener" target="_blank">#PVS</a>

José A. AlonsoFormal verification of quantum stabiliser codes by stabiliser formalism. ~ Qiuyi Feng. <a href="https://people.eng.unimelb.edu.au/rizkallahc/theses/chew-yi-feng-masters-thesis.pdf" rel="nofollow noopener" translate="no" target="_blank">https://people.eng.unimelb.edu.au/rizkallahc/theses/chew-yi-feng-masters-thesis.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#CoqProver</a>

José A. AlonsoReadings shared July 4, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/05-readings_shared_07-04-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/07/05-readings_shared_07-04-25</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rust</a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#TypeTheory</a>

Frühere Suchanfragen

Suchoptionen

Verwaltet von:

Serverstatistik:

#itp