lean-formalizations/CITATION.cff at main · dissensus-ai/lean-formalizations · 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
48
49
50
51
52
53
54
55
56
57
cff-version: 1.2.0
message: "If you use this software, please cite it as below. Do not cite v2.0.0 — see the repository README."
type: software
title: "FarzullaProofs: Lean 4 Formalisations of Definitions and Elementary Algebra"
version: 3.0.0
date-released: 2026-08-25
doi: 10.5281/zenodo.21315610
license: CC-BY-4.0
url: https://github.com/dissensus-ai/lean-formalizations
repository-code: https://github.com/dissensus-ai/lean-formalizations

abstract: >-
  Lean 4 formalisations of the definitions and elementary algebra of research papers by
  Murad Farzulla, checked against Mathlib. Lean verifies that the proofs follow from the
  stated definitions; it does not establish that the definitions faithfully render the
  papers' constructs, and it is not evidence for the papers' substantive claims. Zero
  `sorry` does not mean no unproven assumptions — several modules rest on modelling
  assumptions tracked in ASSUMPTIONS_LEDGER.md. Version 3.0.0 supersedes 2.0.0, which
  formalised a functional retracted on 30 July 2026 and carried self-assigned depth labels
  withdrawn in the August 2026 audit. Nine modules were archived in that audit and are not
  part of this release.

authors:
  - family-names: Farzulla
    given-names: Murad
    orcid: https://orcid.org/0009-0002-7164-8704

keywords:
  - lean4
  - mathlib
  - formalisation

references:
  - type: article
    title: "The Axiom of Consent: Friction Dynamics in Multi-Agent Coordination"
    notes: "The friction functional formalised in this library was retracted on 2026-07-30."
    authors:
      - family-names: Farzulla
        given-names: Murad
    doi: 10.48550/arXiv.2601.06692
    year: 2026

  - type: article
    title: "The Replicator-Optimization Mechanism"
    authors:
      - family-names: Farzulla
        given-names: Murad
    doi: 10.5281/zenodo.18090979
    year: 2026

  - type: article
    title: "Identity is Irreducibly Relational"
    authors:
      - family-names: Farzulla
        given-names: Murad
    doi: 10.5281/zenodo.18186445
    year: 2026