LeanForControl/CITATION.cff at main · math-experiments/LeanForControl · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
cff-version: 1.2.0
message: "If you use this library in your research, please cite it as below."
title: "LeanForControl: A Formal Library for Nonlinear Control Theory in Lean 4"
version: 0.1.0
date-released: 2026-04-18
license: Apache-2.0
repository-code: https://github.com/AnandGokhale/LeanForControl
url: https://anandgokhale.github.io/LeanForControl/
abstract: >
  LeanForControl is a Lean 4 / Mathlib library providing machine-checked
  formalizations of core results in nonlinear control theory. It covers
  comparison functions (class K, K∞, KL), Lyapunov stability theory for
  autonomous and non-autonomous systems, LaSalle's invariance principle,
  input-to-state stability building blocks, and related ODE results.
authors:
  - family-names: Gokhale
    given-names: Anand
    email: anand_gokhale@ucsb.edu
    orcid: ""
  - family-names: Bullo
    given-names: Francesco
    email: bullo@ucsb.edu
    orcid: ""
keywords:
  - lean4
  - formal verification
  - control theory
  - Lyapunov stability
  - comparison functions
  - nonlinear systems
  - interactive theorem proving
  - mathlib
preferred-citation:
  type: software
  title: "LeanForControl: A Formal Library for Nonlinear Control Theory in Lean 4"
  authors:
    - family-names: Gokhale
      given-names: Anand
      email: anand_gokhale@ucsb.edu
    - family-names: Bullo
      given-names: Francesco
      email: bullo@ucsb.edu
  version: 0.1.0
  date-released: 2026-04-18
  license: Apache-2.0
  repository-code: https://github.com/AnandGokhale/LeanForControl
  url: https://anandgokhale.github.io/LeanForControl/