Skip to main content
Proof Assistants Beta

Return to Answer

added 40 characters in body
Source Link
Jason Rute
Jason Rute
  • 10.3k
  • 1
  • 20
  • 57

Your question is unclear. If your question is about practical concerns, I'm not exactly sure what you are asking. Can you define gauge symmetry in Lean or Coq? Also Almost certainly yes! It shouldn't be harder than any other similar area of mathematics.

Can you enumerate the theorems that mention your new concept GaugeSymmetry? I guess, but you would get a bunch of junk like GaugeSymmetry = GaugeSymmetry and (forall∀ (x : GaugeSymmetry), 1=0 -> True. And even without stuff quite so silly, I would be surprised if you find a good solution to this combinatorial explosion.

I think there is some confusion on the terminology of "theory", or of how Lean or Coq is typically used.

Another use case of the terminology "theory" is when one has a completely formal semantics of some mathematical notion. A recent example of this is homotopy type theory, which is a formal language for working directly in something like the infinity groupoid formed by homotopy spaces (I'm probably messing this up). This allows one to do synthetic homotopy theory, proving things about say the homotopy groups of the sphere without having to first go through topological spaces, etc. But, working in a formal system like Lean or Coq doesn't automatically give you a synthetic version of your field. Indeed, despite Lean's foundations being based on dependent type theory, just like homotopy theory, the proofs of Lean's homotopy theoretic results follow similar proofs to those found in the informal literature.

You can, however, prove Bolzano–Weierstrass, and most all other theorems of mathematics, in ZFC (which is also a first-order theory) because ZFC is a more powerful and expressive theory, but without the nice properties of say the theory of real-closed fields. Working in Lean (which is not a first-order logic) is more like working in ZFC. It isn't used for its nice metatheory properties but for its expressiveness and practicality. We don't make a distinction between the Lean or Coq statements that concern, say, groups and those whichthat concern topological spaces. Indeed, it is important that we can talk about both in the same theorem so that we can talk about topological groups for example. Similarly, if you developed gauge symmetry in Lean or Coq, you would have access to all of Lean's or Coq's theorems and definitions for other related fields of mathematics.

Your question is unclear. If your question is about practical concerns, I'm not exactly sure what you are asking. Can you define gauge symmetry in Lean? Also certainly yes! It shouldn't be harder than any other similar area of mathematics.

Can you enumerate the theorems that mention your new concept GaugeSymmetry? I guess, but you would get a bunch of junk like GaugeSymmetry = GaugeSymmetry and (forall x : GaugeSymmetry), 1=0 -> True. And even without stuff quite so silly, I would be surprised if you find a good solution to this combinatorial explosion.

I think there is some confusion on the terminology of "theory", or of how Lean is typically used.

Another use case of the terminology "theory" is when one has a completely formal semantics of some mathematical notion. A recent example of this is homotopy type theory, which is a formal language for working directly in something like the infinity groupoid formed by homotopy spaces (I'm probably messing this up). This allows one to do synthetic homotopy theory, proving things about say the homotopy groups of the sphere without having to first go through topological spaces, etc. But, working in a formal system like Lean doesn't automatically give you a synthetic version of your field. Indeed, despite Lean's foundations being based on dependent type theory, just like homotopy theory, the proofs of Lean's homotopy theoretic results follow similar proofs to those found in the informal literature.

You can, however, prove Bolzano–Weierstrass, and most all other theorems of mathematics, in ZFC (which is also a first-order theory) because ZFC is a more powerful and expressive theory, but without the nice properties of say the theory of real-closed fields. Working in Lean (which is not a first-order logic) is more like working in ZFC. It isn't used for its nice metatheory properties but for its expressiveness and practicality. We don't make a distinction between the Lean statements that concern, say, groups and those which concern topological spaces. Indeed, it is important that we can talk about both in the same theorem so that we can talk about topological groups for example. Similarly, if you developed gauge symmetry in Lean, you would have access to all of Lean's theorems and definitions for other related fields of mathematics.

Your question is unclear. If your question is about practical concerns, I'm not exactly sure what you are asking. Can you define gauge symmetry in Lean or Coq? Almost certainly yes! It shouldn't be harder than any other similar area of mathematics.

Can you enumerate the theorems that mention your new concept GaugeSymmetry? I guess, but you would get a bunch of junk like GaugeSymmetry = GaugeSymmetry and ∀ (x : GaugeSymmetry), 1=0 -> True. And even without stuff quite so silly, I would be surprised if you find a good solution to this combinatorial explosion.

I think there is some confusion on the terminology of "theory", or of how Lean or Coq is typically used.

Another use case of the terminology "theory" is when one has a completely formal semantics of some mathematical notion. A recent example of this is homotopy type theory, which is a formal language for working directly in something like the infinity groupoid formed by homotopy spaces (I'm probably messing this up). This allows one to do synthetic homotopy theory, proving things about say the homotopy groups of the sphere without having to first go through topological spaces, etc. But, working in a formal system like Lean or Coq doesn't automatically give you a synthetic version of your field. Indeed, despite Lean's foundations being based on dependent type theory, just like homotopy theory, the proofs of Lean's homotopy theoretic results follow similar proofs to those found in the informal literature.

You can, however, prove Bolzano–Weierstrass, and most all other theorems of mathematics, in ZFC (which is also a first-order theory) because ZFC is a more powerful and expressive theory, but without the nice properties of say the theory of real-closed fields. Working in Lean (which is not a first-order logic) is more like working in ZFC. It isn't used for its nice metatheory properties but for its expressiveness and practicality. We don't make a distinction between the Lean or Coq statements that concern, say, groups and those that concern topological spaces. Indeed, it is important that we can talk about both in the same theorem so that we can talk about topological groups for example. Similarly, if you developed gauge symmetry in Lean or Coq, you would have access to all of Lean's or Coq's theorems and definitions for other related fields of mathematics.

Source Link
Jason Rute
Jason Rute
  • 10.3k
  • 1
  • 20
  • 57

Your question is unclear. If your question is about practical concerns, I'm not exactly sure what you are asking. Can you define gauge symmetry in Lean? Also certainly yes! It shouldn't be harder than any other similar area of mathematics.

Can you enumerate the theorems that mention your new concept GaugeSymmetry? I guess, but you would get a bunch of junk like GaugeSymmetry = GaugeSymmetry and (forall x : GaugeSymmetry), 1=0 -> True. And even without stuff quite so silly, I would be surprised if you find a good solution to this combinatorial explosion.

But more importantly, I don't understand what you are looking to do here. Why do you want this?

I think there is some confusion on the terminology of "theory", or of how Lean is typically used.

In its most general form, a "theory" in mathematics is when we have stumbled upon the right definitions. In the theory of topology, we have the definitions of topology, open, closed, compact, limit, and so forth. This "theory" forms the basis for a whole new understanding of other areas of mathematics. It sounds like gauge symmetry already has that. So you certainly should be able to write the definition of gauge symmetry in Lean and formalize theorems about it, but I don't think doing that is going to give you any brilliant new insights, except possibly as a way to systematize and record all the known knowledge in this field.

Another use case of the terminology "theory" is when one has a completely formal semantics of some mathematical notion. A recent example of this is homotopy type theory, which is a formal language for working directly in something like the infinity groupoid formed by homotopy spaces (I'm probably messing this up). This allows one to do synthetic homotopy theory, proving things about say the homotopy groups of the sphere without having to first go through topological spaces, etc. But, working in a formal system like Lean doesn't automatically give you a synthetic version of your field. Indeed, despite Lean's foundations being based on dependent type theory, just like homotopy theory, the proofs of Lean's homotopy theoretic results follow similar proofs to those found in the informal literature.

Finally, in logic, "theory" can sometimes mean a very particular thing, namely the set of all statements in some specific logical vocabulary, usually in first-order logic, which holds of a class of objects. Sometimes these theories uniquely classify that family of mathematical objects, like the theory of groups. Other times, they only get as close as you can get in first-order logic, like the first-order theory of the real numbers, which gives rise to the more general notion of a real-closed field. But in both examples, there are lots of important properties that are not expressible in first-order logic, like cyclic groups or the Archemidian property of the reals. Knowing which properties are first-order definable and which aren't is important since the former are preserved by logical gadgets like ultra-products. Also, the first-order theory of the reals is a decidable theory with nice properties like quantifier elimination.

But a first-order theory is usually not the place to prove theorems. You can't do modern group theory in the first-order theory of groups, nor can you do analysis in the first-order theory of the real numbers. It just is not powerful or expressive enough. You can't prove (or even state) Bolzano–Weierstrass in the theory of real-closed fields. For that, you need to bring in all sorts of objects outside of first-order group theory like the integers, set theory, and the like.

You can, however, prove Bolzano–Weierstrass, and most all other theorems of mathematics, in ZFC (which is also a first-order theory) because ZFC is a more powerful and expressive theory, but without the nice properties of say the theory of real-closed fields. Working in Lean (which is not a first-order logic) is more like working in ZFC. It isn't used for its nice metatheory properties but for its expressiveness and practicality. We don't make a distinction between the Lean statements that concern, say, groups and those which concern topological spaces. Indeed, it is important that we can talk about both in the same theorem so that we can talk about topological groups for example. Similarly, if you developed gauge symmetry in Lean, you would have access to all of Lean's theorems and definitions for other related fields of mathematics.