Mathematics - 2017-09-10 (page 4 of 6)

4:00 PM

it's a calculus question

Yeah I think the thing that's scary abt hurricanes is exactly what your saying. It plays out like a prophecy of the end times basically @Semi

Semiclassical

right.

Eric Silva

I think I'm gonna dip off the internet until my parents are capable of reaching me again

Semiclassical

probably a good plan

Harry Evans

4:17 PM

Hello good day!

Quick question: a nonplanar curve always has a curvature, $\kappa \ne 0$, right?

Abcd

4:44 PM

How to get vector using mathjax?

Like arrow over v.

I couldn't find it on the guideline page.

Semiclassical

\vec{v}

Abcd

Thanks.

$\int \vec{F}\cdot\vec{S} = W$

Semiclassical

to get a dot in the middle, use \cdot

so W=\int \vec{F}\cdot d\vec{s}:$W=\int \vec{F}\cdot d\vec{s}$

Abcd

@Semiclassical Is it a notation? Can't dot be placed at the bottom?

Semiclassical

I think having it centered is more typical. But it's not cruicial

Leaky Nun

4:50 PM

0

Q: Lagrange Multiplier isn't working?

Consider the following question: If the constraint function is $g=\pi r^{2}hwu=1$ and the function is $f=4r^{2}wuh$ then using the Lagrange Multiplier system $\lambda=\frac{4}{\pi}$ for all cases. Does that mean that there is no solution or infinite solution? Thanks in advance.

Abcd

@Semiclassical Now how to put it in the middle of the page? I have seen many people posting formulas which appear on the middle not at the corner.

Leaky Nun

every time I see a question titled [XXX isn't working], I have an impulse to reply "no, XXX is working fine, it's you who isn't working"

Semiclassical

$$A=BB$$

like that?

Leaky Nun

how arrogant of the OP to say that they are smarter than Lagrange

Abcd

@Semiclassical yes

Semiclassical

4:52 PM

use \$\$ instead of just one \$

Abcd

$$\int \vec{F}\cdot \vec{S} = W$$ This is cool.

Semiclassical

there's another way to do that (which is more proper) but I never remember it

[ A=B ]

Abcd

@Semiclassical This is tougher way.

Semiclassical

nope, i'm doing it wrong

main issue with what you're writing now is mathematical: integrals should have differentials

$\vec{F}\cdot\vec{S}$ isn't something you integrate

Abcd

Wait. I'll correct it.

Semiclassical

4:55 PM

see here for details: en.wikipedia.org/wiki/…

Abcd

$$\int \vec{F}\cdot d\vec{s} = W$$ @Semiclassical

Semiclassical

right.

where $s(t)$ is your curve

Abcd

@Semiclassical And force is represented by X axis?

Semiclassical

if it was just the x-axis, it wouldn't be a vector

it'd be a component of a vector

@Abcd What?

Abcd

@Semiclassical Please tell what the two axes would represent on the planar graph.

F on x axis?

And S on Y axis?

Semiclassical

4:59 PM

you're making no sense.

Abcd

I am unable to think of the proper preposition I am supposed to use @Semiclassical

Semiclassical

the only way F,S could correspond to axes is if they were scalar quantities.

Abcd

@Semiclassical I know I am not able to express myself clearly.

Semiclassical

look at the animation in the Wikipedia link.

Leaky Nun

@Semiclassical if a logical system is inconsistent, must it be provably inconsistent?

Semiclassical

5:01 PM

no clue.

I'm not a logic guy in that way

Leaky Nun

I thought you know of provability

Semiclassical

a little, but i'm not an expert by any means

Leaky Nun

because I've been playing with Prover9 today

I can't get it to prove $x^+ = y^+ \implies x=y$ though, where $z^+ := z \cup \{z\}$

Semiclassical

i've never played with automated theorem provers, so you'd know better than me at this point

Alex K Chen

Define the function $f:(0,1)\to (0,1)$ by [\displaystyle f(x) = \left\{ \begin{array}{lr} x+\frac 12 & \text{if}\ \ x < \frac 12\\ x^2 & \text{if}\ \ x \ge \frac 12 \end{array} \right.] Let $a$ and $b$ be two real numbers such that $0 < a < b < 1$. We define the sequences $a_n$ and $b_n$ by $a_0 = a, b_0 = b$, and $a_n = f( a_{n -1})$, $b_n = f (b_{n -1} )$ for $n > 0$.

Wait sorry wrong room.

Anyway, why the hell LaTeX doesn't works in Windows Edge (completely dumb browser, you can't fullscreen too) ?

Leaky Nun

5:08 PM

@Semiclassical but is that statement true for arbitrary sets?

hi, @Daminark

lol it can prove $x \notin x$ but not $\neg(x \in y \land y \in x)$

Faust

hey leaky u good at logic right?

Leaky Nun

Let $x$ and $y$ be sets such that $x \in y$ and $y \in x$.
$z=\{x,y\}$ is a set by the axiom of pairing.
$z\ne\varnothing$ because $x \in z$ and $x\notin\varnothing$.
By the axiom of regularity, $\exists a: a \in z \land a \cap z = \varnothing$.
$a \in z$ is equivalent to $a=x \lor a=y$ by the definition of $z$.
If $a=x$, then $y \in a \cap z \ne \varnothing$.
If $a=y$, then $x \in a \cap z \ne \varnothing$.
Contradiction.

@Faust hmm?

If you have a problem I might use the program to solve it :P

Faust

imt rying to do a simple negation

0

Q: Simple negation of statement on graph theory

I am trying to negate the following statement but my logic is alittle rusty... Statment: There exists a set $X \subset V (G) - \{u, v\}$ such that some vertex in X is adjacent to both u and v. My terrible Attempt: For all set's $X \subset V (G) $ then for all $x \in X $ x is adjacent to u or v?...

logic graph-theory

its got some graph theory in it throwing me for a loop

id prefer a hint rather than a full answer

Leaky Nun

@Faust hint given

Faust

thx

i treid to edit it but im not sur eif its better or worse negating the word some is hard

Jasper

5:24 PM

@Faust There is a way to negate statements without thinking.

Leaky Nun

@Faust that's right

Faust

*confused

my negation is right or jaspers statement is right?

Leaky Nun

both are right

Jasper

@Faust Do you know how to negate statements in general?

Faust

in general yes

but the way that was stated was odd

cause i needed to add something in X to negate it

im very very bad at english

like i scored soooo low on the english placement test that they thought i had just arrived in the country

Jasper

5:28 PM

Maybe it has to do with your condition.

Faust

but because my highschool was here it wouldnt let me register for an ESL english course

Anyway thansk guys ill try the next one and see if ic an get it.

Jasper

I agree that one is a little hard to negate.

And sometimes it is not about negating but putting it into a form which you can understand and prove.

Faust

my biggest problem with math is understandin what they are saying

Leaky Nun

@Jasper do you logic?

Faust

luckily the more i do the easier ti seems to get

Jasper

5:32 PM

@LeakyNun All the math I understood was long time ago, boy, lol.

I haven't really done any math for years.

Leaky Nun

@Jasper I can't get my program to prove something it should be able to prove

19 mins ago, by Leaky Nun

lol it can prove $x \notin x$ but not $\neg(x \in y \land y \in x)$

Jasper

I just remember some stuff here and there, like 1+1=2, for example.

@LeakyNun Are you saying there is something wrong with your prog?

Faust

whats the negation of eithier?

Leaky Nun

@Jasper it's a software

Faust

both?

Leaky Nun

5:34 PM

and I don't know what the problem is

Faust

or neither

Leaky Nun

Assumptions:

%definitions
all x all y (subset(x,y) <-> (all z (member(z,x) -> member(z,y)))).
all x all z (member(z,union(x)) <-> (exists t (member(z,t) & member(t,x)))).
all x all z (member(z,singleton(x)) <-> (z=x)).
all x all y all w (member(w,pair(x,y)) <-> ((w=x) | (w=y))).
all x all z (member(z,powerset(x)) <-> subset(z,x)).
all x all y all w (member(w,intersect(x,y)) <-> (member(w,x) & member(w,y))).
all x succ(x) = union(pair(x,singleton(x))).

%axioms
all x all y ((all z (member(z,x) <-> member(z,y))) <-> (x = y)).

MATH ASKER

if the roots of f(x) = 0 are -1, 4 what are the roots for f(1/3x)?

Leaky Nun

Goals:

all x all y -(member(x,y)&member(y,x)).

@MATHASKER f(1/3x) = 0
1/3x = 0 or -1 or 4

Semiclassical

@Faust $\neg(A\wedge B)=\neg A\vee \neg B$

MATH ASKER

5:35 PM

could i just do (x+1)(x-4) instead of x put 1/3?

Jasper

@LeakyNun Haha, is that a problem sheet question from IC you are asked to work on?

Leaky Nun

@Jasper no, it's my exploration with Prover9

MATH ASKER

huh@LeakyNun i didndt get it

Faust

didnt know thats what i was saying

thought i was trying to negate

Leaky Nun

@MATHASKER oops, rewrite:
f(1/3x) = 0
1/3x = -1 or 4

Faust

5:36 PM

$ A \lor B $

Jasper

@LeakyNun You can always ask on the main site. I only know arithmetic now, lol.

Leaky Nun

because you know that the solution of f(y)=0 are y=-1 or y=4 @MATHASKER

@Faust \lor

Faust

how do u say or?

Semiclassical

$\vee$

Leaky Nun

@Semiclassical obviously it's \lor :P

Semiclassical

5:37 PM

lol

Leaky Nun

@Jasper could you go over my assumptions and my goal?

Semiclassical

$\lor$ OR $\vee$

MATH ASKER

oh alright got it thanks @LeakyNun

Leaky Nun

@Faust \neg

Semiclassical

they actually look a little different

$\land$ $\wedge$

$\lor\vee$

Leaky Nun

5:38 PM

@Semiclassical could you go over my assumptions and my goal?

Jasper

@LeakyNun I think no, I am too stupid for that now. =D

Leaky Nun

@Jasper come on

Faust

$ \neg ( A \lor B) = \neg A \land \neg B$ ?

Semiclassical

I'm really not interested. You're the one who dug the hole :P

\land

(logical-and)

Jasper

@LeakyNun That was serious. If you knew me in real life, you would see how pathetic I have become now. =D

Semiclassical

5:39 PM

@Faust yep

Faust

is or = eithier?

Semiclassical

and the same if you swap $\land$ and $\lor$ there

Faust

w8

Semiclassical

well, think about how you use either

Faust

so

Semiclassical

5:40 PM

"Either A or B"

Faust

shit

not same

one sec

Jasper

Before using the symbols, use the words @Faust. Get it right in English first, symbols come later.

Faust

english is confuseing symbols arent ambiguios

Jasper

Symbols are ambiguous when they get complicated.

Then you need the rules for parsing them.

Faust

eithier A or B would be both A and B or Not A and Not B

?

negation obv

Jasper

5:43 PM

Negation of (A or B) is (not A and not B).

Semiclassical

symbols have one obvious advantage: parentheses

Jasper

Negation of (A and B) is (not A or not B).

@Semiclassical So I am cheating by using them now, lol.

Semiclassical

@Faust I think the issue you're after is whether "either A or B" means logical-or or logical-xor

Faust

yes

Semiclassical

i.e. does "either A or B" translate into "exactly one of A,B is true"

Faust

5:44 PM

can or be both?

exactly my confusion

Leaky Nun

use symbols then :P

Jasper

In math writing, (A or B) is always used in the inclusive sense to allow the possibility that both are true.

Leaky Nun

$A \oplus B$ is A xor B

Semiclassical

in logic, OR always allows A and B to be true

Leaky Nun

$A \lor B$ is A or B

Faust

5:45 PM

or both A and B

ok

Jasper

@LeakyNun Ha, we can always redefine the meaning of symbols, lol.

Faust

which is eithier?

i thought eithier was exclusive

Semiclassical

Well, keep in mind: common language != logic

Faust

?

Semiclassical

if someone is working in logic, they'd probably just use symbols in the first place

Faust

5:46 PM

when i say eithier A or B i mean one or the other

Jasper

@Faust Don't worry about the word either in math writing. It doesn't change anything, as far as my use of the word goes. If someone tells you otherwise, then bring it up again.

Faust

what does math mean?

lol

In

Leaky Nun

who is good at logic here?

Semiclassical

oh hey

19

Q: Does "either A or B " preclude "both A and B"?

In mathematics, "A or B" includes "A and B". Does "either" mean "A or B but not (A and B)" or does it include the possibility of "A and B"? The context might be mathematics, formal logic or ordinary language.

conjunctions mathematics logic

Faust

im just going to type out my actual question

Jasper

5:47 PM

@Faust When I say 'either A or B' I mean the same as 'A or B'. And that in math is always used in the inclusive sense.

Faust

yeah i think they broke that with this question though

Leaky Nun

@Jasper update: I had to delete many of the axioms, and the machine used 49.81 seconds to generate the proof...

Semiclassical

and on MSE:

Leaky Nun

% Proof 1 at 49.81 (+ 3.95) seconds.
% Length of proof is 66.
% Level of proof is 12.
% Maximum clause weight is 21.
% Given clauses 10556.

1 (all x all y (subset(x,y) <-> (all z (member(z,x) -> member(z,y))))) # label(non_clause).  [assumption].
2 (all x all y all z (member(z,pair(x,y)) <-> z = x | z = y)) # label(non_clause).  [assumption].
3 (all x all y all z (member(z,intersect(x,y)) <-> member(z,x) & member(z,y))) # label(non_clause).  [assumption].
4 (all x all y ((all z (member(z,x) <-> member(z,y))) <-> x = y)) # label(non_clause).  [assumption].

Semiclassical

5

Q: What is the logical connective for Either.. Or?

I have a statement, Either p or q and I have to write it in terms of logical connectives but I don't get which logical connector should I be using? Here is what I did (I think there could have been a better way to do this) $(p \lor q ) \land (\neg((p \Rightarrow q) \land (q \Rightarrow ...

logic

Jasper

5:48 PM

@Semiclassical Sorry, I have no regard for answers on ELU about math. Plenty of rubbish answers there.

Leaky Nun

(I know that proving is NP)

Semiclassical

well, this isn't just a question about math. it's about how one would interpret the word 'either' if encountered in the world

Jasper

@Semiclassical Yes, but the people on ELU talk about math terms as if they know how mathematicians use it when they don't.

Semiclassical

Point.

Jasper

And I know because I spent 5 years there, lol.

Faust

5:50 PM

For every subset $X \subset V (G) - \{u, v\} $ either every vertex of X is adjacent to u
and nonadjacent to v, or every vertex of X is adjacent to v and nonadjacent
to u.

so in this case can i rewrite this as: For every subset $X \subset V (G) - \{u, v\} $ every (vertex of X is adjacent to u
and nonadjacent to v) or every (vertex of X is adjacent to v and nonadjacent
to u.) and have it still meant he same thing?

Semiclassical

What was the initial statement?

Faust

the top

Jasper

@Faust If someone wanted to use 'or' in the exclusive sense, they write 'A or B, but not both'.

Faust

is that what they have done here yes?

or no...

Semiclassical

"If I pick some vertex other than u,v then it's adjacent to exactly one of u,v."

Faust

5:53 PM

oh thats surprisngly simple

so the and case is removed?

fromt he or

from the or*

im trying to negate the statement but i can't do that will i understand wth it says ;)

Semiclassical

In which case the negation is: "There's some vertex other than u,v which is either adjacent to both u,v or to neither u,v."

Faust

thats what i was trying to acertain

earlier

Semiclassical

The use of "either" isn't ambiguous because the two cases are logically exclusive.

Faust

yeah but i was trying to use it to define the definition of the meaning of eithier

which i then tried to imply it as the definition of or

but in this case its that wierd symbol leaky used

Semiclassical

right. tbh I'd avoid using 'either' except in a case like this where there's no possibility of ambiguity

Jasper

5:57 PM

Either and neither can be pronounced in two ways no matter where you are.

Semiclassical

i.e. if $A\wedge B=F$ then $A\lor B \cong A\oplus B$

Faust

@Semiclassical when you have English comprehension at the grade 6 level its confusing n o matter what

F is false?

Semiclassical

right.

Faust

isomorphic?

no

basically?

Jasper

In math, when we say we have one apple, we may have two apples.

Faust

5:58 PM

well u didnt say exactly one apple

so thats fine

Jasper

If you want to exclude that, then we would say we have exactly one apple.

Semiclassical

"logically equivalent"

Faust

i shouldve asked my whole question in the first place

anyway thanks all of you

Jasper

And by math here, I mean higher math. School math is a whole nother game altogether.

No kindergarten teacher is going to tell the kids exactly one apple.

Faust

which is the problem i hav with the english language

Jasper

6:01 PM

In this case, it is not about English.

Faust

there are rules that some people follow and others that don't

Jasper

It is about conventions used in mathematical writing.

Faust

so i dont know what set of ruels the indivual is using

Jasper

Also note that some authors may use very weird conventions.

Faust

perhaps not english then people?

Jasper

6:01 PM

It's just life. Life is hard.

Faust

i compose data on them and try and aggregate it to understand them but they are seemingly random never following a boolean path

Jasper

Data on people?

Faust

it took me a very very long time to understand on some level humans

Jasper

LOL

Faust

sarcasm was especially hard to understand

i still often misunderstand

Jasper

6:03 PM

And is that because of your condition again?

Faust

and people say one thing but actually they think anthor

i dont do that

well i try and hold my toungue because apperntly its bad to say the truth sometimes

but its bad to lie

Jasper

There are many reasons why people say one thing and think another.

Faust

people are one big contradition

Jasper

If you can't say the truth at least don't tell lies.

Faust

thats what i do

but its still ahrd to tell when i should avoid the truth

Little Rookie

6:04 PM

Anyone can help me on a problem of Gambler's ruin?

Im getting really stressed up :(

Faust

my friends accept as a very honest blunt person but others can often find me offencive

Jasper

Well, you just need to continue observing people and work on your interpersonal skills.

Faust

the worst part is i never know cause people don't say what they think

anyway i should so some more hw

Leaky Nun

my software solved B(2,3) within a fraction of a second... a few days earlier I spent hours working on it

Assumptions:


all x all y all z ((x*y)*z = x*(y*z)). %G1
all x x*e=x. %G2
all x x*inv(x)=e. %G3
all x x*(x*x)=e. %B(2,3).

Goals:

all x all y x*y=y*x.

Output:

interpretation( 27, [number = 1,seconds = 0], [
    function(*(_,_), [
         0, 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,
         1, 2, 0, 9,15,17,20,10,11,12,13,14, 3, 7, 8,16, 4,18, 5,23,21, 6,24,25,26,19,22,
         2, 0, 1,12,16,18,21,13,14, 3, 7, 8, 9,10,11, 4,15, 5,17,25, 6,20,26,19,22,23,24,
         3, 7, 8, 4, 0, 1, 2, 5, 6,21,16,18,17,20,15,26,23,22,25, 9,24,19,12,10,13,11,14,
         4, 5, 6, 0, 3, 7, 8, 1, 2,19,23,25,22,24,26,14,10,12,11,21,13, 9,17,16,20,18,15,

1

A: The order of the group $\langle a, b| w^3, w\in\langle a, b\rangle\rangle$ for $w$ being any word.

Prerequisite: $$\begin{array}{rcl} (a^mb^n)^3 &=& e \\ a^mb^na^mb^na^mb^n &=& e \\ b^na^mb^n &=& a^{3-m}b^{3-n}a^{3-m} \end{array}$$ Then we fill the following table row by row from top to bottom, each row from left to right, being mindful to collisions described above, and creating new rows as...

Abcd

6:17 PM

Solve the inequality for integral values of x:
$$\sqrt{-x^2+10x-16}<x-2$$
$$\implies x-2> 0 \implies x\in(2,\infty)$$
Then, squaring both sides:$$(x-2)(x-5)>0$$
$$\implies x\in (-\infty,2)\cup(5,\infty)$$
Intersecting the two results, $$x\in (5, +\infty)$$
Thus, there are infinite integral solutions but answer given is $$ {6,7,8} $$
Where have I gone wrong(any alternate way?)?
PS: Please ignore the above question if it's busywork/ looks like 0 effort homework problem/ useless/ it wastes your time.

How to get {} (which represent point solutions) using math jax?

Leaky Nun

@Abcd \{

Abcd

Answer given is $$\{6,7,8\}$$

Leaky Nun

hint: you need the LHS to be defined

Abcd

@LeakyNun defined?

Leaky Nun

@Abcd yes, defined.

@Secret the proof of the F(2,5) problem (to determine that $a^11=1$):

Faust

6:22 PM

0

Q: Negation of logical statement in graph theory

I am given the following statement i am going to attempt to translate it into something alitle easier for me to understand then negate it. Statement: For every set $ X \subset V(G) - \{ u,v \} $ either every vertex of X is adjacent to u and nonadjacent to v, or every vertex is adjacent to v and...

logic graph-theory

So does this all make sense?

Abcd

@LeakyNun It is defined.

Leaky Nun

@Abcd not for every value of $x$.

Abcd

@LeakyNun Ah, I see. You mean $\sqrt{y}>0 $, where $y= -x^2+10x-16$

Leaky Nun

@Abcd yes.

Abcd

Got the answer @LeakyNun :-) . Thanks for the hint.

Leaky Nun

6:26 PM

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 111.
% Level of proof is 25.
% Maximum clause weight is 91.
% Given clauses 40.

1 (all x all y all z (x * y) * z = x * (y * z)) # label(non_clause).
2 (all x x * 1 = x) # label(non_clause).
3 (all x x * inv(x) = 1) # label(non_clause).
4 a * (a * (a * (a * (a * (a * (a * (a * (a * (a * a))))))))) = 1 # label(non_clause) # label(goal).

@Secret ^

Abcd

I hope you meant it's not defined in this situation only @LeakyNun because square root of negative numbers is defined too.

Leaky Nun

@Abcd sure

@AlessandroCodenotti hi

Alessandro Codenotti

Hi chat

Faust

i still messed it up

i need to do a few more of these

Leaky Nun

9

Q: Is there a short proof of $x^2=(-x)^2$ in an arbitrary ring?

Identity: Let $R$ be a ring and $x \in R$. Then $x^2=(-x)^2.$ It's exam marking time here, and one of the students used the above identity in a proof. The identity is true, but I can't think of a straightforward proof of this. Question: Is there a short proof of this identity? (Note:...

abstract-algebra ring-theory

Prover9 at work :D @AlessandroCodenotti

Jasper

6:42 PM

@LeakyNun You must be really excited to go to school. =D

Leaky Nun

@Jasper I am.

Jasper

@LeakyNun Well, I hope you will be a great mathematician in future. Don't forget me when you win the Fields medal, lol.

Leaky Nun

@Jasper heh

Jasper

There is one particular topic whose books I never explored.

Abcd

@LeakyNun Do you aspire to be a mathematician?

Jasper

6:45 PM

And that is books which teach students how to write proofs at the start of their undergrad studies.

Any recommendations for this?

Leaky Nun

@Jasper no idea

Tobias Kildetoft

@Jasper I quite like Chapter Zero, though it is on the expensive side

Leaky Nun

@Abcd maybe

Jasper

@TobiasKildetoft LOL Aluffi also has Algebra Chapter 0, LOL.

Abcd

@LeakyNun All the best! You will surely be a great one!

Leaky Nun

6:46 PM

@Abcd thanks

Tobias Kildetoft

@Jasper This one is just called Chapter Zero. It is by Carol Schumacher

Leaky Nun

Prover9 is really fun lol

Tobias Kildetoft

(I may not have spelled that name correctly)

Jasper

I can't remember how I learnt to write proofs myself.

I think it must have been a combination of learning some basic logic and reading some basic number theory books.

Tobias Kildetoft

I learned from that book (as part of a course following it)

Leaky Nun

6:49 PM

@TobiasKildetoft do you logic?

Tobias Kildetoft

@LeakyNun Not if I can help it :)

Leaky Nun

@TobiasKildetoft what do you mean?

Tobias Kildetoft

Though I did take a course on mathematical logic (and even TA'ed it the following year)

Jasper

@LeakyNun I think it means he doesn't like it very much, lol.

Tobias Kildetoft

I am not very fond of the technicalities that come with studying logic formally

Leaky Nun

6:50 PM

@TobiasKildetoft do you know anyone that does?

Jasper

When you study logic too much, you might become illogical. Sad thing that happened to Kurt Godel.

Tobias Kildetoft

I don't think so

Leaky Nun

Given a group where $x+x=0$ for all $x$, prove that the group is abelian:

1 x + y = y + x # label(non_clause) # label(goal).  [goal].
2 x + (y + z) = (x + y) + z.  [assumption].
3 (x + y) + z = x + (y + z).  [copy(2),flip(a)].
4 x + 0 = x.  [assumption].
6 x + x = 0.  [assumption].
7 c2 + c1 != c1 + c2.  [deny(1)].
8A x + y = x + (0 + y).  [para(4(a,1),3(a,1,1))].
8 x + (0 + y) = x + y.  [copy(8A),flip(a)].
11 0 + x = y + (y + x).  [para(6(a,1),3(a,1,1))].
12A 0 = x + (y + (x + y)).  [para(6(a,1),3(a,1))].
12 x + (y + (x + y)) = 0.  [copy(12A),flip(a)].
19A 0 + x = x + 0.  [para(6(a,1),11(a,2,2))].

this one is quite short

Jasper

@LeakyNun So this program mechanically proves theorems?

Sha Vuklia

Guys, let $R$ be a ring with $1\neq 0$ and $T=\{\begin{pmatrix}a&b\\c&d\end{pmatrix}\in M(2,R)\mid c=0\}$. I’ve shown that $\begin{pmatrix}a&b\\c&d\end{pmatrix}\in T^*\iff a\in R^*\text{ and }d\in R^*$. I now need to show that if $T^*$ is commutative, then $R^*=\{1\}$. I’ve tried all kinds of things now, but I just kind of want to know what direction I should choose. Should I go for contraposition or a direct proof?

Leaky Nun

6:52 PM

@Jasper yes

@ShaVuklia don't worry, I won't give you a mechanical proof ;)

Jasper

@LeakyNun Too bad this kind of program can only do simple things, otherwise it would solve all the hard problems as well. Maybe it's a good thing, so that humans still have something to do that machines cannot.

Sha Vuklia

lol alright

Leaky Nun

@Jasper proof generation is NP if I recall correctly

Tobias Kildetoft

@ShaVuklia So just assume there is some non-trivial unit in $R$ and use that to construct to matrices in $T^*$ that do not commute.

Jasper

@LeakyNun If you play Go (Wei Qi) you might know that Cambridge math prof Imre Leader is a Go expert.

Leaky Nun

6:54 PM

I have to point out that $M(2,R)$ does not make sense since $R$ is not a field

Tobias Kildetoft