Differences

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

--- meetings_spring_2026 [2026/02/10 15:32] – [February 4] asjensen
+++ meetings_spring_2026 [2026/06/01 22:09] (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     | The Combined p-Dirichlet and p-Thomson Principles on Planar Maps | Pietro Poggi-Corradini | Kansas State Univeristy | [[#april_15|Abstract]] |
-| April 22     |  |  |  |
+| April 22     | Safety Verification of AI-Enabled Autonomous Systems: A Formal Approach | Lipsy Gupta | Kansas State Univeristy | [[#april_22|Abstract]] |
-| April 29     |  |  |  |
+| April 29     | Geodesic Trees and bi-Lipschitz Embeddings | Manisha Garg | University of Illinois Urbana-Champaign | [[#april_29|Abstract]] |
-| May 6        |  |  |  |
+| May 6        | The Goldfarb-Idnani Approach for Computing Modulus | Nalen Rangarajan | Kansas State University | [[#may_6|Abstract]] |
 ===== 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∃∀N", Nathan Albin**\\
+**"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.
+==== April 15 ====
+**"The Combined p-Dirichlet and p-Thomson Principles on Planar Maps", Pietro Poggi-Corradini**\\
+I will describe how the $p\neq 2$ case can be handled on planar orthodiagonal maps, by introducing a new "combined" energy that takes contributions from both primal and the dual edges.
+==== April 22 ====
+**"Safety Verification of AI-Enabled Autonomous Systems: A Formal Approach", Lipsy Gupta**\\
+As neural networks are increasingly integrated into safety-critical systems such as autonomous vehicles, robots, and aerospace systems, a fundamental question arises: can we prove that such a system will never enter an unsafe state? This talk introduces formal safety verification for neural network-controlled dynamical systems, with reachability analysis as the core technical challenge. We survey verification approaches and note that scalability remains a central challenge. We then present a reduction technique based on approximate bisimilarity that constructs a provably close smaller network from a large one, making verification more tractable. No background in AI or machine learning is assumed.
+==== April 29 ====
+**"Geodesic Trees and bi-Lipschitz Embeddings", Manisha Garg**\\
+A natural question in the bi-Lipschitz geometry of trees is whether a large class of geodesic trees admits a single universal element, that is, a fixed tree into which every member of the class embeds in a bi-Lipschitz manner. Furthermore, Kinnenberg asked if every quasiconformal tree of Assouad dimension < 2 admits a bi-Lipschitz embedding into R^2. Chrontsios-Garitsis, Ioannidis, and Vellis prove that the class of quasiconformal trees with uniform separation can quasisymmetrically embed into a universal element T, and moreover, this T admits a biLipschitz embedding into R^2. In this talk, we will show that such a universal element cannot be found if one replaces quasisymmetric maps with bi-Lipschitz maps, not even in the case of the geodesic trees. This answers a question of the aforementioned authors. This is joint work with Sylvester Eriksson-Bique.
+==== May 6 ====
+**"The Goldfarb-Idnani Approach for Computing Modulus", Nalen Rangarajan**\\
+The Goldfarb-Idnani algorithm is a dual-based method for solving
+quadratic programs in general. Here, we present an overview of the algorithm in the special case that arises in modulus.