Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
ruby.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
If you are interested in the Ruby programming language, come join us! Tell us about yourself when signing up. If you just want to join Mastodon, another server will be a better place for you.

Administered by:

Server stats:

1.1K
active users

ruby.social: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#math

81 posts53 participants13 posts today
Public
José A. Alonso

Verified program extraction in number theory: The fundamental theorem of arithmetic and relatives. ~ Franziskus Wiesnet. arxiv.org/abs/2504.03460 #ITP #Minlog #Haskell #FunctionalProgramming #Math

arXiv logo
arXiv.orgVerified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and RelativesThis article revisits standard theorems from elementary number theory through a constructive, algorithmic, and proof-theoretic lens, within the theory of computable functionals. Key examples include Bèzout's identity, the fundamental theorem of arithmetic, and Fermat's factorization method. All definitions and theorems are fully formalized in the proof assistant Minlog, thereby laying the foundation for a comprehensive formal framework for number theory within Minlog. While formalization ensures correctness, our primary emphasis is on the computational content of proofs. Leveraging Minlog's built-in program extraction, we obtain executable terms that are exported as Haskell code. Efficiency of the extracted programs plays a central role. We show how performance considerations influence even the initial formulation of theorems and proofs. In particular, we compare formalizations based on binary encodings of natural numbers with those using the traditional unary (successor-based) representation. We present several core proofs in detail and reflect on the challenges that arise from formalization in contrast to informal reasoning. The complete formalisation is available online and linked for reference. Minlog's tactic scripts are designed to follow the structure of natural-language proofs, allowing each derivation step to be traced precisely and helping to bridge the gap between formal and classical mathematical reasoning.
Replied in thread
Public
Rowan Brad Quni

@paninid fast forward to the present and scientists who barely study #philosophy label #metaphysics as #pseudoscience (forgetting what #PhD means), torment #logic for the benefit of "elegant" #math equations (e.g. antimatter, dark #matter), and design #AI #systems that weaponize #ethics as justification for #information #censorship (#ChatGPT "knows" but refuses to answer how to a hot wire a car or commit murder while claiming no #opinion, ignorant that words and actions are different)

Continued thread
Public
⏚ Antoine Chambert-Loir

This is where a new variant of the criterion can be applied, this time with the prime number 3.

Indeed, modulo 3, one has f(T)=T^4+2T^2+1=(T^2+1)^2.
So we are almost as in the initial criterion, but the polynomial T is not T^2+1.

The first thing that makes this criterion apply is that T^2+1 is irreducible modulo 3. In this case, this is because -1 is not a square mod 3.

The criterion also requires of variant of the condition on the derivative — it holds because the polynomial is not zero modulo (T^2+1, 9). Here, one has
T^4-10T^2+1=(T^2+1)^2-12T^2 = (T^2+1)^2-12(T^2+1)+12 is equal to 3 modulo (T^2+1, 9).

And so we have an Eisenstein-type proof that the polynomial T^4-10T^2+1 is irreducible over the integers. CQFD.
#math

Public *
⏚ Antoine Chambert-Loir

(#math thread)
Recently, in the Zulip server for Lean users, somebody went with something that looked like homework, but managed to sting me a little bit.

It was about irreducibility of polynomials with integer coefficients. Specifically, the guy wanted a proof that the polynomial T^4-10 T^2+1 is irreducible, claiming that the Eisenstein criterion was not good at it.

What was to proven (this is what *irreducible* means) is that it is impossible to write that polynomial as the product of two polynomials with integer coefficients, except by writing
T^4-10 T^2+1 as (1)·(T^4-10 T^2+1) or as (-1)·(-T^4+10 T^2-1).

ExploreLive feeds
About