Differences

This shows you the differences between two versions of the page.

--- meetings_spring_2026 [2026/02/10 15:32] – [February 11] asjensen
+++ meetings_spring_2026 [2026/04/07 13:58] (current) – asjensen
@@ Line 2: / Line 2: @@
 //All meetings take place on Wednesdays, 2:30 - 3:30 pm in Burt Hall 204 unless otherwise noted.//
-^ Date ^ Meeting Title ^ Speaker ^ Abstract ^
+^ Date ^ Meeting Title ^ Speaker ^ University ^ Abstract ^
-| February 4   | Getting L∃∀N | Nathan Albin | [[#february_4|Abstract]] |
+| February 4   | Getting L∃∀N | Nathan Albin | Kansas State University | [[#february_4|Abstract]] |
-| February 11  | Getting L∃∀Ner | Nathan Albin | [[#february_11|Abstract]] |
+| February 11  | Getting L∃∀Ner | Nathan Albin | Kansas State University | [[#february_11|Abstract]] |
-| February 18  |  |  |  |
+| February 18  | A L∃∀N Handshake | Nathan Albin | Kansas State University | [[#february_18|Abstract]] |
-| February 25  |  |  |  |
+| February 25  | Base Modulus for Matroid Truncation, Strength, and Fractional Arboricity | Huy Truong | Kansas State University | [[#february_25|Abstract]] |
-| March 4      |  |  |  |
+| March 4      | Modulus of Families of Lipschitz Chains with Arbitrary Dimension and Codimension | Andrew Jensen | Kansas State University | [[#march_4|Abstract]] |
-| March 11     |  |  |  |
+| March 11     | **NO MEETING** |  |  |  |
-| March 18     | **NO MEETING** | //Spring Break// |  |
+| March 18     | **NO MEETING** | | | |
-| March 25     |  |  |  |
+| March 25     | **NO MEETING** |  | | |
-| April 1      |  |  |  |
+| April 1      | **NO MEETING** |  | | |
-| April 8      |  |  |  |
+| April 8      | Hamilton-Jacobi Equations on Graphs with Applications to Semi-Supervised Learning and Data Depth  | Andrew Jensen | Kansas State University | [[#april_8_|Abstract]] |
-| April 15     |  |  |  |
+| April 15     |  |  | | |
-| April 22     |  |  |  |
+| April 22     |  |  | | |
-| April 29     |  |  |  |
+| April 29     |  |  | | |
-| May 6        |  |  |  |
+| May 6        |  |  | | |
 ===== Abstracts =====
@@ Line 24: / Line 24: @@
 This semester, I've decided it's time to learn to use the programming language (and interactive theorem prover) Lean (lean-lang.org). To support this goal, I'm planning to lead informal demonstrations and discussions at a few NODE meetings. This will be the first of those. I'm about as far from being an expert as one can get, but I'll show you the ε > 0 that I've learned thus far. In keeping with the unofficial acronym NODE = Nathan Often Does Examples, I'll work through some constructions and proofs using "easy" structures like the natural numbers, and we can explore questions as they arise. I may get to the point of proving the handshaking lemma in graph theory. If not, that will be for a future installment. Eventually, I'll be proving things about p-modulus with an AI assistant.
-==== February 11  ====
+==== February 11 ====
 **"Getting L∃∀Ner", Nathan Albin**\\
 Continuing with the Lean theme, I'll start from an empty Lean file and show how to use inductive types to construct the natural numbers from scratch and how to prove theorems about them. It's also a good time to talk about the Curry–Howard isomorphism, which establishes the link between logic and computation. You'll often see this summarized as "propositions are types, proofs are programs." This means proof-checking is really just type-checking in disguise. I find this dual view incredibly helpful; if I get stuck thinking about a logical implication, I can switch to thinking about writing a function with a specific type signature.
+==== February 18 ====
+**"A L∃∀N Handshake", Nathan Albin**\\
+I could talk for hours about inductive types, type checking, and "proofs as programs." But I won't inflict that on the group (for now). This time, we'll start delving into the gigantic repository of proofs called the Mathlib. If you want to build mathematical proofs without constantly reinventing the wheel, this is the library you need. Although graphs and the handshaking lemma are already included in the library, we'll pretend they're not and build them ourselves using more fundamental objects, like sets. This will give a sense of how bundled mathematical structures are defined, and of how frustrating it can be to search through the library for a lemma or theorem that you know _must_ exist. (AI can help sometimes, but it tends to be overconfident.) We'll also encounter our friend Lem (the Law of the Excluded Middle) once again and learn how Lean handles noncomputable terms. That will come in handy when we start dealing with the real numbers.
+==== February 25 ====
+**"Base Modulus for Matroid Truncation, Strength, and Fractional Arboricity", Huy Truong**\\
+In previous work, we studied the p-modulus of the family of all bases of a matroid and showed that it recovers several classical concepts in matroid theory, including strength, fractional arboricity, and principal partitions. These results generalize corresponding concepts for spanning trees in graphs. Due to computational constraints, one may impose a bound on the number of elements sampled from a base. For instance, when exploring a tree, we may stop at forests with $t$ edges. Such objects are captured by matroid truncations. In this paper, we study the modulus of matroid truncations and determine the universal density for every truncation of a given matroid. As a consequence, we show that the truncation modulus serves as an approximation of the original matroid modulus.
+==== March 4 ====
+**"Modulus of Families of Lipschitz Chains with Arbitrary Dimension and Codimension", Andrew Jensen**\\
+Recently, Lohvansuu (2023) introduced the p-modulus for families of k-dimensional Lipschitz chains and their dual families of (n-k)-dimensional chains. While he established an upper bound for the duality of these families on Lipschitz cubes, the corresponding lower bound remained an open question. Subsequently, Kangasniemi and Prywes (2025) developed dMod, a related notion of modulus based on differential forms, and successfully established a full duality result. In this talk, I will explore the implications of these developments and discuss related open problems.
+==== April 8 ====
+**"Hamilton-Jacobi Equations on Graphs with Applications to Semi-Supervised Learning and Data Depth", Andrew Jensen**\\
+We will be reading through a paper by Jeff Calder and Mahmood Ettehad discussing how the p-Eikonal Equation on graphs allows one to recover distances on graphs, and in particular p -> infinity recovers shortest-path graph distance. The authors then apply the finding in machine learning contexts. I will briefly share an overview of the paper's results, then the remaining portion of the meeting will be a group discussion on the paper. You can find the paper at https://arxiv.org/abs/2202.08789.