Re: [Lurch] Introduction.

[Ken M. <ken...@gm...>]

Welcome!

I'm glad to hear that you are thinking about using Lurch in your Number
Theory course next fall.

I am currently teaching and Introduction to Proof course at my university
using Lurch, and as part of that course I am developing an very elementary
Number Theory library that is intended for students in that course.  Since
my course is not a full-blown course on Number Theory it will only contain
Lurch rules for induction, divisibility, gcd, lcm, primes, composites, and
congruence.  We do not actually define the natural numbers from axioms (but
have some rules for recognizing, integer constants and doing arithmetic
with them) since I'm really only doing elementary naive set theory and
number theory with the focus being on teaching the students how to write
mathematical proofs.

If you have only a few additional specific topics you would like to see
included I would be happy to include them to customize it to your needs. If
you require a more substantial number theory package, perhaps doing an
axiomatic construction of the natural numbers along the lines of the
Peanoaxioms or constructing the natural numbers in
ZFC, I would be happy to work with you to develop it.

I have middle school level math education majors (a new certification in
Pennsylvania) in my current course, and so far they are handling Lurch and
the abstraction of the Intro to Proof course quite well.

Let me know what topics and definitions you would like to use in your
course and we can best plan how to move forward from there.

-KEN