Wikipedia:Reference desk/Mathematics

Welcome to the mathematics section
of the Wikipedia reference desk.

skip to bottom

Select a section:

• Computing
• Entertainment
• Humanities
• Language
• Mathematics
• Science
• Miscellaneous
• Archives

Want a faster answer?

Main page: Help searching Wikipedia

   

How can I get my question answered?

• Select the section of the desk that best fits the general topic of your question (see the navigation column to the right).
• Post your question to only one section, providing a short header that gives the topic of your question.
• Type '~~~~' (that is, four tilde characters) at the end – this signs and dates your contribution so we know who wrote what and when.
• Don't post personal contact information – it will be removed. Any answers will be provided here.
• Please be as specific as possible, and include all relevant context – the usefulness of answers may depend on the context.
• Note:
  • We don't answer (and may remove) questions that require medical diagnosis or legal advice.
  • We don't answer requests for opinions, predictions or debate.
  • We don't do your homework for you, though we'll help you past the stuck point.
  • We don't conduct original research or provide a free source of ideas, but we'll help you find information you need.

Ready? Ask a new question!

How do I answer a question?

Main page: Wikipedia:Reference desk/Guidelines

• The best answers address the question directly, and back up facts with wikilinks and links to sources. Do not edit others' comments and do not give any medical or legal advice.

See also:

• Teahouse
• Help desk
• Village pump
• Help manual

September 12

Can Rocq/Coq produce actual proofs?

I've been looking at the proof assistant Rocq (recently Coq) but in the demos I've seen it's always an interactive process that verifies the statement without actually producing a proof that humans can follow. For example in the our article where they prove that 0 is even the proof goes:

Proof. reflexivity. Qed.

I was hoping for something a bit more specific and readable like "By the initial step in the inductive definition." If Rocq can't do this, is there another proof assistant that can? --RDBury (talk) 19:36, 12 September 2026 (UTC)

Reportedly (I have never used it myself), ACL2 outputs a description of its formal steps in natural language. ("The proofs that ACL2 discovers are printed in a very verbose but readable English format." See the input and output of an ACL2 proof of the irrationality of √2.  ​‑‑Lambiam 10:24, 13 September 2026 (UTC)

Thanks, I check it out. I was thinking that Isabelle looked promising as well, but it's hard to know for sure without learning the program. That seems to be the common theme: there are about a dozen proof assistants available, but they all seem to require that you spend at least a week to get the basics of using them, and there's no guarantee that you'll be able to do what you want to do after that investment. It seems like the barrier to entry is larger than I was hoping for. Meanwhile I've been doing proofs without an assistant for decades now, so even though I want to keep an open mind, it seems hard to justify adding another learning curve to automate something I already know how to do. --RDBury (talk) 21:19, 13 September 2026 (UTC)

September 14

Underlying structure for semigroupoid

Reflexive quivers are used as underlying structures in small category, and multiplicative graphs, but what about semigroupoid? Since each vertex doesn't need to have an identity and (but) the composition of pair of consecutive morphisms appears to always be defined, so I don't think it's based on a reflexive quiver. The statement "composition of pair of consecutive morphisms is always defined", I might be overlooking additional conditions. I'm worried about case of the composition of endomorphism (loop) and ordinary morphism with with same source or target.--SilverMatsu (talk) 04:21, 14 September 2026 (UTC)

I'm sorry, but I find the definition given for reflexive quivers hard to understand. Assuming that reflexive quivers are quivers, I think the definition should take the form of defining a reflexive quiver as being a quiver with an additional requirement, and use the notation of the Definition section to formulate that requirement. Also, the meanings of the notations $1_{G_{0}}$ and $\mathrm {loop} (x)$ are not given. I assume $1_{G_{0}}$ stands for the identity function ${\text{id}}_{G_{0}},$ but this may not be clear to all readers.  ​‑‑Lambiam 06:53, 14 September 2026 (UTC)

Thank you for pointing that out. I added a figure.--SilverMatsu (talk) 09:19, 14 September 2026 (UTC)

For example, I think for loop edge $\mathrm {id} _{B}$ to be an identity arrow, it requires that composition $g\circ \mathrm {id} _{B}$ and $\mathrm {id} _{B}\circ f$ are defined.(IMO) Also, quiver does not require composition.--SilverMatsu (talk) 04:35, 15 September 2026 (UTC)

What should we call the following axiom (in multiplicative graph#Definition)? Axiom 1: For each element $x$ of ${\underline {\Sigma }}$, the composites $x\circ \alpha (x)$ and $\beta (x)\circ x$ are defined, and we have $x\circ \alpha (x)=x=\beta (x)\circ x.$ Here, $\alpha (x)$ is the right identity of $x$ and is called the source of $x$, while $\beta (x)$ is the left identity of $x$ and is called the target of $x$. Should this axiom be called "existence of units" or "existence of composition for loops"? There might be a better term for "existence of composition for loops".--SilverMatsu (talk) 03:13, 18 September 2026 (UTC)

A semigroupoid is, in general, not a reflexive quiver. In particular, we can have a degenerate semigroupoid with just objects and only empty sets of morphisms – and therefore no loops.  ​‑‑Lambiam 08:53, 18 September 2026 (UTC)

Thank you for explaining with an example.--SilverMatsu (talk) 02:48, 20 September 2026 (UTC)