41554 blogs · [ { "id": "01a087e2-3424-70da-8797-af5480946791", "title": "IsarMathLib 1.35.0: Update to Isabelle 2025-1, Uniformities and pseudometrics", "url": "https://slawekk.wordpress.com/2025/12/20/isarmathlib-1-35-0-update-to-isabelle-2025-1-uniformities-and-pseudometrics/", "published_at": "2025-12-20T13:09:34+00:00" }, { "id": "01a087e2-3424-70da-8797-af5480a2a2f9", "title": "IsarMathLib 1.34.0: Z-modules and complete lattice of uniformities", "url": "https://slawekk.wordpress.com/2025/08/24/isarmathlib-1-34-0-z-modules-and-complete-lattice-of-uniformities/", "published_at": "2025-08-24T07:03:45+00:00" }, { "id": "01a087e2-3425-713e-b6c9-37772c8ea563", "title": "IsarMathLib 1.33.0: ultrafilters, ultraproducts, hypernaturals, order on uniformities", "url": "https://slawekk.wordpress.com/2025/05/18/isarmathlib-1-33-0-ultrafilters-ultraproducts-hypernaturals-order-on-unformities/", "published_at": "2025-05-18T13:33:38+00:00" }, { "id": "01a087e2-3425-713e-b6c9-37772d47e92f", "title": "IsarMathLib 1.32.0: Update to Isabelle2025 and Uniformity from collection of pseudometrics", "url": "https://slawekk.wordpress.com/2025/03/19/isarmathlib-1-32-0-update-to-isabelle2025-and-uniformity-from-collection-of-pseudometrics/", "published_at": "2025-03-19T18:40:17+00:00" }, { "id": "01a087e2-3425-713e-b6c9-37772dfb7c01", "title": "Panel Discussion on Formalization in Mathematics", "url": "https://slawekk.wordpress.com/2024/08/05/panel-discussion-on-formalization-in-mathematics/", "published_at": "2024-08-05T12:08:13+00:00" }, { "id": "01a087e2-3425-713e-b6c9-37772e26e8b2", "title": "IsarMathLib 1.31.0: Pseudometric spaces as uniform spaces", "url": "https://slawekk.wordpress.com/2024/07/27/isarmathlib-1-31-0-pseudometric-spaces-as-uniform-spaces/", "published_at": "2024-07-27T09:05:39+00:00" }, { "id": "01a087e2-3425-713e-b6c9-37772f0ce40e", "title": "IsarMathLib 1.30.0: Modules and update to Isabelle2024", "url": "https://slawekk.wordpress.com/2024/05/28/isarmathlib-1-30-0-modules-and-update-to-isabelle2024/", "published_at": "2024-05-28T16:26:00+00:00" }, { "id": "01a087e2-3425-713e-b6c9-37772fa7abd8", "title": "IsarMathLib 1.29.0: Modules and vector spaces", "url": "https://slawekk.wordpress.com/2024/03/25/isarmathlib-1-29-0-modules-and-vector-spaces/", "published_at": "2024-03-25T18:12:59+00:00" }, { "id": "01a087e2-3425-713e-b6c9-37772fcc6755", "title": "Variance swaps in a CAS", "url": "https://slawekk.wordpress.com/2023/10/08/variance-swaps-in-a-cas/", "published_at": "2023-10-08T17:01:08+00:00" }, { "id": "01a087e2-3425-713e-b6c9-37773075c30b", "title": "IsarMathLib 1.28.1: Update to Isabelle2023", "url": "https://slawekk.wordpress.com/2023/09/15/isarmathlib-1-28-1-update-to-isabelle2023/", "published_at": "2023-09-15T17:04:40+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d081e696b5f", "title": "IsarMathLib 1.28.0: Binomial theorem", "url": "https://slawekk.wordpress.com/2023/05/07/isarmathlib-1-28-0-binomial-theorem/", "published_at": "2023-05-07T18:59:46+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d081edc4a62", "title": "IsarMathLib 1.27.0: Spectrum of a quotient ring, Finite State Machines", "url": "https://slawekk.wordpress.com/2023/03/18/isarmathlib-1-27-0-spectrum-of-a-quotient-ring-finite-state-machines/", "published_at": "2023-03-18T14:57:00+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d081f081479", "title": "IsarMathLib 1.26.0: Ring ideals and Zariski topology", "url": "https://slawekk.wordpress.com/2023/01/30/isarmathlib-1-26-0-ring-ideals-and-zariski-topology/", "published_at": "2023-01-30T19:17:45+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d081fa5191c", "title": "IsarMathLib 1.25.0: Comparison with Metamath", "url": "https://slawekk.wordpress.com/2022/12/28/isarmathlib-1-25-0-comparison-with-metamath/", "published_at": "2022-12-28T18:28:38+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d082011979c", "title": "IPC with F# and Fable.Remoting", "url": "https://slawekk.wordpress.com/2022/12/11/ipc-with-f-and-fable-remoting/", "published_at": "2022-12-11T11:00:27+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d0820e810e3", "title": "IsarMathLib 1.24.0: Update to Isabelle2022", "url": "https://slawekk.wordpress.com/2022/10/29/isarmathlib-1-24-0-update-to-isabelle2022/", "published_at": "2022-10-29T19:23:56+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d0821a5dc48", "title": "IsarMathLib 1.23.0: Rewrite of the presentation layer in F#", "url": "https://slawekk.wordpress.com/2022/09/05/isarmathlib-1-23-0-rewrite-of-the-presentation-layer-in-f/", "published_at": "2022-09-05T19:33:37+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d0821fd5ffc", "title": "Summing up in Kaitai Struct", "url": "https://slawekk.wordpress.com/2022/01/08/summing-up-in-kaitai-struct/", "published_at": "2022-01-08T10:06:02+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d08222a0831", "title": "IsarMathLib 1.22.1: Update to Isabelle2021-1", "url": "https://slawekk.wordpress.com/2021/12/25/isarmathlib-1-22-1-update-to-isabelle2021-1/", "published_at": "2021-12-25T16:34:18+00:00" }, { "id": "01a0d052-69fa-725b-b09e-5d082233fc2d", "title": "IsarMathLib 1.22.0: Uniform covers part II", "url": "https://slawekk.wordpress.com/2021/10/05/isarmathlib-1-22-0-uniform-covers-part-ii/", "published_at": "2021-10-05T16:58:31+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e5891ca1", "title": "IsarMathLib 1.21.0: Uniform covers", "url": "https://slawekk.wordpress.com/2021/08/22/isarmathlib-1-21-0-uniform-covers/", "published_at": "2021-08-22T16:26:29+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e58fea54", "title": "IsarMathLib 1.20.0: Ordered loops and loop valued metrics", "url": "https://slawekk.wordpress.com/2021/04/28/isarmathlib-1-20-0-ordered-loops-and-loop-valued-metrics/", "published_at": "2021-04-28T11:27:40+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e68e7ade", "title": "IsarMathLib 1.19.0: Loops", "url": "https://slawekk.wordpress.com/2021/04/06/isarmathlib-1-19-0-loops/", "published_at": "2021-04-06T15:31:03+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e6ea3d7d", "title": "IsarMathLib 1.18.0: Quasigroups", "url": "https://slawekk.wordpress.com/2021/03/24/isarmathlib-1-18-0-quasigroups/", "published_at": "2021-03-24T16:50:41+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e71fb743", "title": "IsarMathLib 1.17.0: Real numbers as a metric and topological space", "url": "https://slawekk.wordpress.com/2021/03/07/isarmathlib-1-17-0-real-numbers-as-a-metric-and-topological-space/", "published_at": "2021-03-07T09:27:39+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e7828d55", "title": "IsarMathLib version 1.16.0: metric spaces", "url": "https://slawekk.wordpress.com/2021/02/01/isarmathlib-version-1-16-0-metric-spaces/", "published_at": "2021-02-01T16:59:08+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e7c7584b", "title": "IsarMathLib version 1.15.0: comparison with Mizar", "url": "https://slawekk.wordpress.com/2020/12/13/isarmathlib-version-1-15-0-comparison-with-mizar/", "published_at": "2020-12-13T15:41:48+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e846e231", "title": "IsarMathLib version 1.14.0: lattices", "url": "https://slawekk.wordpress.com/2020/09/29/isarmathlib-version-1-14-0-lattices/", "published_at": "2020-09-29T17:46:32+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e8c79826", "title": "IsarMathLib version 1.13.0: Roelcke uniformity", "url": "https://slawekk.wordpress.com/2020/08/03/isarmathlib-version-1-13-0/", "published_at": "2020-08-03T10:04:00+00:00" }, { "id": "01a0d052-d99d-7217-8ea7-9ce8e951f177", "title": "IsarMathLib version 1.12.1: update to Isabelle2020", "url": "https://slawekk.wordpress.com/2020/05/12/isarmathlib-version-1-12-1/", "published_at": "2020-05-12T17:38:28+00:00" }, { "id": "01a0d053-2543-737f-8882-5e32000e6ab3", "title": "IsarMathLib version 1.12.0: topological groups and uniformities", "url": "https://slawekk.wordpress.com/2020/05/05/isarmathlib-version-1-12-0/", "published_at": "2020-05-05T17:00:39+00:00" }, { "id": "01a0d053-2543-737f-8882-5e3200c8559b", "title": "IsarMathLib version 1.11.0: uniform spaces", "url": "https://slawekk.wordpress.com/2020/02/11/isarmathlib-version-1-11-0/", "published_at": "2020-02-11T16:19:37+00:00" }, { "id": "01a0d053-2543-737f-8882-5e3200cdd790", "title": "IsarMathLib version 1.10.0: neighborhood systems", "url": "https://slawekk.wordpress.com/2019/11/23/isarmathlib-version-1-10-0/", "published_at": "2019-11-23T13:53:03+00:00" }, { "id": "01a0d053-2543-737f-8882-5e32018aba27", "title": "Lean and Metamath Zero", "url": "https://slawekk.wordpress.com/2019/11/10/lean-and-metamath-zero/", "published_at": "2019-11-10T08:30:37+00:00" }, { "id": "01a0d053-2543-737f-8882-5e3201920163", "title": "IsarMathLib version 1.9.8 released", "url": "https://slawekk.wordpress.com/2019/08/29/isarmathlib-version-1-9-8-released/", "published_at": "2019-08-29T16:51:36+00:00" }, { "id": "01a0d053-2543-737f-8882-5e32022e0eaa", "title": "FMM 2018 and IsarMathLib release 1.9.7", "url": "https://slawekk.wordpress.com/2018/08/26/fmm-2018-and-isarmathlib-release-1-9-7/", "published_at": "2018-08-26T14:37:28+00:00" }, { "id": "01a0d053-2543-737f-8882-5e32027ab52a", "title": "IsarMathLib updated to Isabelle2016-1", "url": "https://slawekk.wordpress.com/2017/03/20/isarmathlib-updated-to-isabelle2016-1/", "published_at": "2017-03-20T08:45:52+00:00" }, { "id": "01a0d053-2543-737f-8882-5e3202902f92", "title": "Visualizing Pandas GroupBy object", "url": "https://slawekk.wordpress.com/2017/03/15/visualizing-pandas-groupby-object/", "published_at": "2017-03-15T09:49:01+00:00" }, { "id": "01a0d053-2543-737f-8882-5e3202fd40d7", "title": "Cheap air quality monitoring", "url": "https://slawekk.wordpress.com/2017/01/16/cheap-air-quality-monitoring/", "published_at": "2017-01-16T17:03:48+00:00" }, { "id": "01a0d053-2543-737f-8882-5e3203175809", "title": "IsarMathLib 1.9.4 and other news", "url": "https://slawekk.wordpress.com/2016/04/17/isarmathlib-1-9-4-and-other-news/", "published_at": "2016-04-17T18:49:04+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbeb79d783a", "title": "IsarMathLib 1.9.3 released", "url": "https://slawekk.wordpress.com/2015/06/30/isarmathlib-1-9-3-released/", "published_at": "2015-06-30T14:37:45+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbeb851f44f", "title": "Air Quality Egg", "url": "https://slawekk.wordpress.com/2015/05/26/air-quality-egg/", "published_at": "2015-05-26T11:01:13+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbeb86d2112", "title": "FOM discussion", "url": "https://slawekk.wordpress.com/2014/10/25/fom-discussion/", "published_at": "2014-10-25T11:01:59+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbeb909b4d3", "title": "IsarMathLib 1.9.2 released", "url": "https://slawekk.wordpress.com/2014/10/20/isarmathlib-1-9-2-released/", "published_at": "2014-10-20T11:15:27+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbeb932f49f", "title": "Binary comprehensions in Erlang", "url": "https://slawekk.wordpress.com/2014/09/19/binary-comprehensions-in-erlang/", "published_at": "2014-09-19T15:28:09+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbeb9db378f", "title": "Mathgate", "url": "https://slawekk.wordpress.com/2014/07/30/mathgate/", "published_at": "2014-07-30T08:56:43+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbeba0bf4d6", "title": "KDB+, Elm and web sockets", "url": "https://slawekk.wordpress.com/2014/07/15/kdb-elm-and-web-sockets/", "published_at": "2014-07-15T12:25:49+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbeba9ea848", "title": "Game of Life with Enterprise Components", "url": "https://slawekk.wordpress.com/2014/05/20/game-of-life-with-enterprise-components/", "published_at": "2014-05-20T15:28:22+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbebb999a71", "title": "ProofPeer", "url": "https://slawekk.wordpress.com/2014/02/01/proofpeer/", "published_at": "2014-02-01T12:41:54+00:00" }, { "id": "01a0d053-7bdd-7385-9bd9-7dbebc1789b2", "title": "Proof market", "url": "https://slawekk.wordpress.com/2014/01/11/proof-market/", "published_at": "2014-01-11T08:59:58+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6d96999e", "title": "Bitcoin epic fails", "url": "https://slawekk.wordpress.com/2014/01/04/bitcoin-epic-fails/", "published_at": "2014-01-04T14:39:31+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6dd5e1af", "title": "IsarMathLib version 1.9.1 released", "url": "https://slawekk.wordpress.com/2014/01/03/isarmathlib-version-1-9-1-released/", "published_at": "2014-01-03T07:58:50+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6e1f48f3", "title": "Java, Mockito and ArgumentCaptor", "url": "https://slawekk.wordpress.com/2013/09/03/java-mockito-and-argumentcaptor/", "published_at": "2013-09-03T11:17:45+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6e42c1c3", "title": "IsarMathLib 1.9.0 released", "url": "https://slawekk.wordpress.com/2013/07/26/isarmathlib-1-9-0-released/", "published_at": "2013-07-26T07:51:48+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6e8925f8", "title": "Gowers and Ganesalingam", "url": "https://slawekk.wordpress.com/2013/05/12/gowers-and-ganesalingam/", "published_at": "2013-05-12T13:25:01+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6ea3a8e0", "title": "IsarMathLib 1.8.0 released", "url": "https://slawekk.wordpress.com/2013/02/25/isarmathlib-1-8-0-released/", "published_at": "2013-02-25T13:34:53+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6ef9d4c0", "title": "Scala", "url": "https://slawekk.wordpress.com/2012/10/26/scala/", "published_at": "2012-10-26T13:37:15+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6fac38ce", "title": "IsarMathLib 1.7.5", "url": "https://slawekk.wordpress.com/2012/10/09/isarmathlib-1-7-5/", "published_at": "2012-10-09T07:36:50+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6fae337b", "title": "Installing Isabelle", "url": "https://slawekk.wordpress.com/2012/09/17/installing-isabelle/", "published_at": "2012-09-17T18:50:08+00:00" }, { "id": "01a0d053-c47f-701c-abba-093e6fde862d", "title": "The Russell proof language", "url": "https://slawekk.wordpress.com/2012/08/19/the-russell-proof-language/", "published_at": "2012-08-19T11:07:40+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da4957304", "title": "IsarMathLib 1.7.4", "url": "https://slawekk.wordpress.com/2012/06/30/isarmathlib-1-7-4/", "published_at": "2012-06-30T12:44:05+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da5656b83", "title": "Recently read", "url": "https://slawekk.wordpress.com/2012/01/26/recently-read/", "published_at": "2012-01-26T13:09:55+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da6492088", "title": "IsarMathLib 1.7.2", "url": "https://slawekk.wordpress.com/2011/07/20/isarmathlib-1-7-2/", "published_at": "2011-07-20T18:11:16+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da72541b6", "title": "IsarMathLib 1.7.1", "url": "https://slawekk.wordpress.com/2011/05/13/isarmathlib-1-7-1/", "published_at": "2011-05-13T09:32:46+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da75851ae", "title": "The first formalized math wiki is here", "url": "https://slawekk.wordpress.com/2011/04/13/the-first-formalized-math-wiki-is-here/", "published_at": "2011-04-13T11:50:05+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da79dd4fe", "title": "Isabelle2011, IsarMathLib 1.7.0 and other news", "url": "https://slawekk.wordpress.com/2011/02/19/isabelle2011-isarmathlib-1-7-0-and-other-news/", "published_at": "2011-02-19T14:48:01+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da7e5e6a3", "title": "The next generation of proof assistants: ten questions", "url": "https://slawekk.wordpress.com/2010/11/17/the-next-generation-of-proof-assistants-ten-questions/", "published_at": "2010-11-17T11:44:59+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da84cc111", "title": "New versions of Isabelle, I3P and IsarMathLib", "url": "https://slawekk.wordpress.com/2010/07/11/new-versions-of-isabelle-i3p-and-isarmathlib/", "published_at": "2010-07-11T19:07:37+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da9021975", "title": "How to Publish Counterexamples in 1 2 3 Easy Steps", "url": "https://slawekk.wordpress.com/2010/05/21/how-to-publish-counterexamples-in-1-2-3-easy-steps/", "published_at": "2010-05-21T12:19:13+00:00" }, { "id": "01a0d054-1122-7013-8390-8e7da9a7644c", "title": "Goodbye ProofGeneral, again", "url": "https://slawekk.wordpress.com/2010/04/04/goodbye-proofgeneral-again/", "published_at": "2010-04-04T19:00:42+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b783fcf9b1", "title": "Gödel, Chaitin and formalized mathematics", "url": "https://slawekk.wordpress.com/2010/03/23/godel-chaitin-and-formalized-mathematics/", "published_at": "2010-03-23T18:52:22+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b7845bdcc7", "title": "Q – six months later", "url": "https://slawekk.wordpress.com/2010/02/13/q-six-months-later/", "published_at": "2010-02-13T08:51:24+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b78550002e", "title": "Isabelle 2009-1 and IsarMathLib", "url": "https://slawekk.wordpress.com/2009/12/05/isabelle-2009-1-and-isarmathlib/", "published_at": "2009-12-05T17:33:28+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b7863d15d4", "title": "Markov chains – simulation", "url": "https://slawekk.wordpress.com/2009/08/01/markov-chains-simulation/", "published_at": "2009-08-01T01:32:33+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b786e2c363", "title": "Haskell in Q", "url": "https://slawekk.wordpress.com/2009/07/24/haskell-in-q/", "published_at": "2009-07-24T01:54:03+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b787abb1f2", "title": "Moving again", "url": "https://slawekk.wordpress.com/2009/07/22/moving-again/", "published_at": "2009-07-22T21:59:24+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b787bacc89", "title": "IsarMathLib version 1.6.9 released", "url": "https://slawekk.wordpress.com/2009/07/07/isarmathlib-version-1-6-9-released/", "published_at": "2009-07-07T23:06:58+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b788517477", "title": "Formalpedia", "url": "https://slawekk.wordpress.com/2009/06/15/formalpedia/", "published_at": "2009-06-15T08:22:20+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b7887cd3b6", "title": "Markov chains", "url": "https://slawekk.wordpress.com/2009/06/05/markov-chains/", "published_at": "2009-06-05T02:00:44+00:00" }, { "id": "01a0d054-5adc-72fe-8deb-70b78939c4e6", "title": "Probability monad", "url": "https://slawekk.wordpress.com/2009/05/31/probability-monad/", "published_at": "2009-05-31T22:39:43+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfb8ee106", "title": "IsarMathLib version 1.6.8 released", "url": "https://slawekk.wordpress.com/2009/04/26/isarmathlin-version-168-released/", "published_at": "2009-04-26T00:17:52+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfbfa8ffe", "title": "Isabelle 2009 released", "url": "https://slawekk.wordpress.com/2009/04/22/isabelle-2009-released/", "published_at": "2009-04-22T00:06:10+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfc4d2b74", "title": "MathWiki project is hiring", "url": "https://slawekk.wordpress.com/2009/03/10/mathwiki-project-is-hiring/", "published_at": "2009-03-10T21:38:57+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfc97e21b", "title": "Interval arithmetic in groups – pass 2", "url": "https://slawekk.wordpress.com/2009/03/01/interval-arithmetic-in-groups-pass-2/", "published_at": "2009-03-01T21:49:41+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfcb08e31", "title": "IsarMathLib version 1.6.7 released", "url": "https://slawekk.wordpress.com/2009/02/18/isarmathlib-version-167-released/", "published_at": "2009-02-18T01:53:59+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfcd8eb0c", "title": "Goodbye ProofGeneral", "url": "https://slawekk.wordpress.com/2009/01/15/goodbye-proofgeneral/", "published_at": "2009-01-15T00:17:13+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfd47cff2", "title": "Formalmath.org", "url": "https://slawekk.wordpress.com/2009/01/07/formalmathorg/", "published_at": "2009-01-07T23:43:39+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfd972f52", "title": "What next after Tiddly Formal Math?", "url": "https://slawekk.wordpress.com/2008/12/29/what-next-after-tiddly-formal-math/", "published_at": "2008-12-29T23:22:06+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfd9b781b", "title": "IsarMathLib 1.6.6 released", "url": "https://slawekk.wordpress.com/2008/12/19/isarmathlib-166-released/", "published_at": "2008-12-19T23:04:59+00:00" }, { "id": "01a0d054-98a7-71d2-bc7d-3bfcfe4a69aa", "title": "Interval arithmetic in groups: Pass 1", "url": "https://slawekk.wordpress.com/2008/12/06/interval-arithmetic-in-groups-pass-1/", "published_at": "2008-12-06T22:57:20+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b4fd4086", "title": "Vdash, monotone and ikiwiki", "url": "https://slawekk.wordpress.com/2008/11/18/monotone-ikiwiki-and-vdash/", "published_at": "2008-11-18T02:26:15+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b5f52aa4", "title": "Formal Proof II", "url": "https://slawekk.wordpress.com/2008/11/09/formal-proof-ii/", "published_at": "2008-11-09T02:53:23+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b6aa1f4a", "title": "Formal Proof I", "url": "https://slawekk.wordpress.com/2008/11/08/fromal-proof-i/", "published_at": "2008-11-08T02:56:43+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b6c7eb9a", "title": "Formalized Mathematics in the Notices of the AMS", "url": "https://slawekk.wordpress.com/2008/11/06/formalized-mathematics-in-notices-of-the-ams/", "published_at": "2008-11-06T23:21:41+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b702eecf", "title": "1/0 = 0, really!", "url": "https://slawekk.wordpress.com/2008/10/14/10-0-really/", "published_at": "2008-10-14T23:05:37+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b771a157", "title": "Math Wiki news", "url": "https://slawekk.wordpress.com/2008/10/11/math-wiki-news/", "published_at": "2008-10-11T23:54:28+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b86c4ec2", "title": "The Great Bailout", "url": "https://slawekk.wordpress.com/2008/10/03/the-great-bailout/", "published_at": "2008-10-03T23:23:30+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b86df087", "title": "IsarMathLib version 1.6.5 relased", "url": "https://slawekk.wordpress.com/2008/09/27/isarmathlib-version-165-relased/", "published_at": "2008-09-27T00:53:52+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b8db404e", "title": "Vdash", "url": "https://slawekk.wordpress.com/2008/09/18/vdash/", "published_at": "2008-09-18T00:57:56+00:00" }, { "id": "01a0d054-d42b-72a1-ba8a-cba0b8e20478", "title": "Formalizing three dots", "url": "https://slawekk.wordpress.com/2008/08/24/formalizing-three-dots/", "published_at": "2008-08-24T17:04:38+00:00" } ] posts Claim your blog

Back to slawekk.wordpress.com

Blog · corpus.blog/blogs/slawekk.wordpress.com/posts

slawekk.wordpress.com

slawekk.wordpress.com

2025

IsarMathLib 1.35.0: Update to Isabelle 2025-1, Uniformities and pseudometrics original ↗

20 Dec 2025

IsarMathLib 1.34.0: Z-modules and complete lattice of uniformities original ↗

24 Aug 2025

IsarMathLib 1.33.0: ultrafilters, ultraproducts, hypernaturals, order on uniformities original ↗

18 May 2025

IsarMathLib 1.32.0: Update to Isabelle2025 and Uniformity from collection of pseudometrics original ↗

19 Mar 2025

2024

Panel Discussion on Formalization in Mathematics original ↗

5 Aug 2024

IsarMathLib 1.31.0: Pseudometric spaces as uniform spaces original ↗

27 Jul 2024

IsarMathLib 1.30.0: Modules and update to Isabelle2024 original ↗

28 May 2024

IsarMathLib 1.29.0: Modules and vector spaces original ↗

25 Mar 2024

2023

Variance swaps in a CAS original ↗

8 Oct 2023

IsarMathLib 1.28.1: Update to Isabelle2023 original ↗

15 Sept 2023

IsarMathLib 1.28.0: Binomial theorem original ↗

7 May 2023

IsarMathLib 1.27.0: Spectrum of a quotient ring, Finite State Machines original ↗

18 Mar 2023

IsarMathLib 1.26.0: Ring ideals and Zariski topology original ↗

30 Jan 2023

2022

IsarMathLib 1.25.0: Comparison with Metamath original ↗

28 Dec 2022

IPC with F# and Fable.Remoting original ↗

11 Dec 2022

IsarMathLib 1.24.0: Update to Isabelle2022 original ↗

29 Oct 2022

IsarMathLib 1.23.0: Rewrite of the presentation layer in F#original ↗

5 Sept 2022

Summing up in Kaitai Struct original ↗

8 Jan 2022

2021

IsarMathLib 1.22.1: Update to Isabelle2021-1 original ↗

25 Dec 2021

IsarMathLib 1.22.0: Uniform covers part II original ↗

5 Oct 2021

IsarMathLib 1.21.0: Uniform covers original ↗

22 Aug 2021

IsarMathLib 1.20.0: Ordered loops and loop valued metrics original ↗

28 Apr 2021

IsarMathLib 1.19.0: Loops original ↗

6 Apr 2021

IsarMathLib 1.18.0: Quasigroups original ↗

24 Mar 2021

IsarMathLib 1.17.0: Real numbers as a metric and topological space original ↗

7 Mar 2021

IsarMathLib version 1.16.0: metric spaces original ↗

1 Feb 2021

2020

IsarMathLib version 1.15.0: comparison with Mizar original ↗

13 Dec 2020

IsarMathLib version 1.14.0: lattices original ↗

29 Sept 2020

IsarMathLib version 1.13.0: Roelcke uniformity original ↗

3 Aug 2020

IsarMathLib version 1.12.1: update to Isabelle2020 original ↗

12 May 2020

IsarMathLib version 1.12.0: topological groups and uniformities original ↗

5 May 2020

IsarMathLib version 1.11.0: uniform spaces original ↗

11 Feb 2020

2019

IsarMathLib version 1.10.0: neighborhood systems original ↗

23 Nov 2019

Lean and Metamath Zero original ↗

10 Nov 2019

IsarMathLib version 1.9.8 released original ↗

29 Aug 2019

2018

FMM 2018 and IsarMathLib release 1.9.7 original ↗

26 Aug 2018

2017

IsarMathLib updated to Isabelle2016-1 original ↗

20 Mar 2017

Visualizing Pandas GroupBy object original ↗

15 Mar 2017

Cheap air quality monitoring original ↗

16 Jan 2017

2016

IsarMathLib 1.9.4 and other news original ↗

17 Apr 2016

2015

IsarMathLib 1.9.3 released original ↗

30 Jun 2015

Air Quality Egg original ↗

26 May 2015

2014

FOM discussion original ↗

25 Oct 2014

IsarMathLib 1.9.2 released original ↗

20 Oct 2014

Binary comprehensions in Erlang original ↗

19 Sept 2014

Mathgate original ↗

30 Jul 2014

KDB+, Elm and web sockets original ↗

15 Jul 2014

Game of Life with Enterprise Components original ↗

20 May 2014

ProofPeer original ↗

1 Feb 2014

Proof market original ↗

11 Jan 2014

Bitcoin epic fails original ↗

4 Jan 2014

IsarMathLib version 1.9.1 released original ↗

3 Jan 2014

2013

Java, Mockito and ArgumentCaptor original ↗

3 Sept 2013

IsarMathLib 1.9.0 released original ↗

26 Jul 2013

Gowers and Ganesalingam original ↗

12 May 2013

IsarMathLib 1.8.0 released original ↗

25 Feb 2013

2012

Scala original ↗

26 Oct 2012

IsarMathLib 1.7.5 original ↗

9 Oct 2012

Installing Isabelle original ↗

17 Sept 2012

The Russell proof language original ↗

19 Aug 2012

IsarMathLib 1.7.4 original ↗

30 Jun 2012

Recently read original ↗

26 Jan 2012

2011

IsarMathLib 1.7.2 original ↗

20 Jul 2011

IsarMathLib 1.7.1 original ↗

13 May 2011

The first formalized math wiki is here original ↗

13 Apr 2011

Isabelle2011, IsarMathLib 1.7.0 and other news original ↗

19 Feb 2011

2010

The next generation of proof assistants: ten questions original ↗

17 Nov 2010

New versions of Isabelle, I3P and IsarMathLib original ↗

11 Jul 2010

How to Publish Counterexamples in 1 2 3 Easy Steps original ↗

21 May 2010

Goodbye ProofGeneral, again original ↗

4 Apr 2010

Gödel, Chaitin and formalized mathematics original ↗

23 Mar 2010

Q – six months later original ↗

13 Feb 2010

2009

Isabelle 2009-1 and IsarMathLib original ↗

5 Dec 2009

Markov chains – simulation original ↗

1 Aug 2009

Haskell in Q original ↗

24 Jul 2009

Moving again original ↗

22 Jul 2009

IsarMathLib version 1.6.9 released original ↗

7 Jul 2009

Formalpedia original ↗

15 Jun 2009

Markov chains original ↗

5 Jun 2009

Probability monad original ↗

31 May 2009

IsarMathLib version 1.6.8 released original ↗

26 Apr 2009

Isabelle 2009 released original ↗

22 Apr 2009

MathWiki project is hiring original ↗

10 Mar 2009

Interval arithmetic in groups – pass 2 original ↗

1 Mar 2009

IsarMathLib version 1.6.7 released original ↗

18 Feb 2009

Goodbye ProofGeneral original ↗

15 Jan 2009

Formalmath.org original ↗

7 Jan 2009

2008

What next after Tiddly Formal Math?original ↗

29 Dec 2008

IsarMathLib 1.6.6 released original ↗

19 Dec 2008

Interval arithmetic in groups: Pass 1 original ↗

6 Dec 2008

Vdash, monotone and ikiwiki original ↗

18 Nov 2008

Formal Proof II original ↗

9 Nov 2008

Formal Proof I original ↗

8 Nov 2008

Formalized Mathematics in the Notices of the AMS original ↗

6 Nov 2008

1/0 = 0, really!original ↗

14 Oct 2008

Math Wiki news original ↗

11 Oct 2008

The Great Bailout original ↗

3 Oct 2008

IsarMathLib version 1.6.5 relased original ↗

27 Sept 2008

Vdash original ↗

18 Sept 2008

Formalizing three dots original ↗

24 Aug 2008