User talk:Slawekk

From Wikipedia, the free encyclopedia

Welcome!

Hello Slawekk, and welcome to Wikipedia! Thank you for your contributions. I hope you like the place and decide to stay. Here are a few good links for newcomers:

I hope you enjoy editing here and being a Wikipedian! Please sign your name on talk pages using four tildes (~~~~); this will automatically produce your name and the date. If you have any questions, check out Wikipedia:Where to ask a question or ask me on my talk page. Again, welcome!  RJFJR 03:30, 15 December 2005 (UTC)

[edit] Isabelle

Hello, and also a warm welcome from me. I saw your remark that having a link to a formally verified proof of a theorem certainly increases "authoritativeness", on Wikipedia talk:WikiProject Mathematics/Archive9. You might not know it, but that page contains archived discussions, which means that not many people will read your remark.

You propose to add links to formally verified proofs to Wikipedia articles. If you just want to add links to a few articles, just go ahead. If you want to add many links, it might be better to discuss it first. The proper place is probably Wikipedia talk:WikiProject Mathematics (so not the archive). I don't have much of an opinion about it myself. I am not familiar with proof systems and the proofs do not seem very useful to me. You are right that the proof is short, at least the proof that you showed, but I still find it hard to read (that may be because I never did ZF). But it's an interesting idea.

You also uploaded Image:Isar example.png. As far as I could see, you have not used this image anywhere. What do you want to do with it? I'm asking because perhaps you are having trouble including it in an article and you could use some help.

I hope to see you around. Let me know on User talk:Jitse Niesen if you require help or clarification. Cheers, Jitse Niesen (talk) 10:55, 15 December 2005 (UTC)

I uploaded Image:Isar example.png in the sandbox just to see how it will look like for a Wikipedia user in a browser. It looked bad. I would remove it, but I read somewhere in the documentation that only admins can remove uploaded stuff.
I do need help with what I want to do. My plan is to include a link to the proof as an internal link in the Isabelle entry. The point is that the example Isabelle proof there is somewhat misleading as it shows the old, "apply" command based style. Many Isabelle users still use it, but most would use the newer "declarative" style that is easier to follow for a casual reader. The file at [1] is in pdf format and I can not find any reference in the documentation how to include an internal link to a file that is not a (jpeg or png) image. --Slawekk 17:23, 15 December 2005 (UTC)

I deleted the file for you. The 'official' procedure is explained at WP:CSD, but it's often easier to ask an admin personally.

As far as I know, it is not possible to use internal links to a PDF file. I think your best bet is to include the proof as text. Do you use Isabelle yourself? It looks like the PDF file is generated from LaTeX output, so you could include the LaTeX in the article and amend the LaTeX formatting commands. -- Jitse Niesen (talk) 17:42, 15 December 2005 (UTC)

Thanks for the information. Yes, I use Isabelle. I am the (only so far) developer of IsarMathLib. Isabelle uses Latex to generate that pdf file in some very sophisticated way that I don't think can be ported to Wikipedia Latex facilities (at least I don't know how to do that). Isabelle generates it from a source which is a text file, but I don't want to show that one. It would be like showing the Latex source of a matematical paper, not really interesting for a reader.
Do you think using an external link like this one [2] would be acceptable? --Slawekk 18:32, 15 December 2005 (UTC)

I'm sure that will be fine. -- Jitse Niesen (talk) 21:53, 15 December 2005 (UTC)

If you generate PDF from LaTeX, you can try my translation tool to generate wikicode automatically. Jmath666 00:33, 4 June 2007 (UTC)