@user21 hi user21, when would the internship start precisely?

@xzczd "Funny, LaplaceTransform[1//Sin, 1, 1] evaluates to 1/2." I think it just did the same as sol = LaplaceTransform[Sin[x], x, x] which gives 1/(1 + x^2) then replacing x by 1 gives 1/2. May be more type checking is needed to make sure the input makes sense. This is why LaplaceTransform[Sin[2],2,2] gives 1/5.

@Alucard in principal the internship can start immediately but a later point in time is also possible, it's quite flexible. If you have more questions let me know.

@user21 can we talk in a different chatroom? i don't want to bother the others with notification that they may not find interesting

@Alucard, you can reach me at ruebenko AT wolfram.com

@user21 thanks, i will write you an email then.

although it's just a thought i had. maybe the others will forgive me if i abuse of this chatroom a little longer. the thing is i need to pick my last free class this semester and i was already thinking to take a course on numerical resolution of pde from the department of mathematics. now since the website says " spring 2020" and spring ends june 22 i thought i may have a shot at passing the selection process if the internship start later (end of may +-).

On the contrary, if it's too late i will simply inform some of my friends who maybe have already taken the course and may be interested.

right now i mean

Hey. Been out for a year and a half or so. Messing around with FindEquationalProof. Read all the questions about it on here and WC. Still stuck on something simple. So if we do a standard representation of integers as 0, s[0], s[s[0]], s[s[s[0]]], etc. And a couple of simple axioms for additions, why can it easily prove that 1+1 == 2 but runs forever instead of returning false for 1+1 == 3?

axioms={
ForAll[a,a==plus[a,0]],
ForAll[{a,b},plus[a,s[b]]==s[plus[a,b]]]
};
FindEquationalProof[s[s[0]]==plus[s[0],s[0]],axioms]
FindEquationalProof[s[s[s[0]]]==plus[s[0],s[0]],axioms]

I mean I know that's a property of the algorithm used that it might run forever, but I thought this example might be simple enough for it to definitively say false.

Although I thought the whole point of the Knuth-Bendix algorithm was that it's supposed to recognize confluence/canonical forms so that once it gets to expressions that only have s[s[...[0]]] it should know that if the expressions aren't equal then they won't ever be equal no matter how much it messes with them.